Unify order.

Lebesgue/Set_theory/Set_system/Topology.v

@@ -34,7 +34,7 @@ Proof.
 destruct HPB as [HPB1 HPB2]; rewrite <- HT; apply Open_ext.
 (* *)
 intros A HA; rewrite (HPB2 _ HA).
-pose (PB_A := fun B => incl B A /\ PB B); fold PB_A.
+pose (PB_A := fun B => PB B /\ incl B A); fold PB_A.
 destruct (empty_dec PB_A) as [H | H].
 (* . *)
 rewrite empty_equiv in H; rewrite H, unionp_any_nullary.
@@ -56,7 +56,7 @@ Qed.
 Lemma Basisp_Union_any_inter : Union_any_inter PB.
 Proof.
 destruct HPB as [HPB1 HPB2]; intros B1 B2 HB1 HB2.
-exists (fun B => incl B (inter B1 B2) /\ PB B); split; try easy.
+exists (fun B => PB B /\ incl B (inter B1 B2)); split; try easy.
 apply HPB2; rewrite <- HT; apply Open_Inter; apply Open_Gen; auto.
 Qed.