Unify order (with Set_system_any).

Lebesgue/Set_theory/Set_system/Set_system_def_any.v

@@ -69,12 +69,13 @@ Definition is_Basisf : set (Idx -> set U) :=
   fun fB =>
     (forall i, T (fB i)) /\
     (forall A, T A ->
-      A = unionf_any (fun i => inter (prop_cst (incl (fB i) A)) (fB i))).
+      A = unionf_any (fun i => inter (fB i) (prop_cst (incl (fB i) A)))).
 
+(* FIXME: using (Subset A PB) generates pbs in Set_system_any/is_Basisf_is_Basisp_equiv! *)
 Definition is_Basisp : set_system_class U :=
   fun PB =>
     (Incl PB T) /\
-    (forall A, T A -> A = unionp_any (fun B => incl B A /\ PB B)).
+    (forall A, T A -> A = unionp_any (fun B => PB B /\ incl B A)).
 
 End Basis_Def1.