Add result (need to change the name ;)

Lebesgue/Set_theory/Set_system/Set_system_any.v

@@ -419,14 +419,7 @@ intros PB; rewrite <- (unskolem_skolem PB) at 1.
 apply iff_sym, is_Basisf_is_Basisp_equiv.
 Qed.
 
-End Basis_Facts1.
-
-
-Section Basis_Facts2.
-
-Context {U : Type}.
-
-Variable T : set_system U.
+(** Equivalent definitions. *)
 
 Lemma is_Basisf_equiv :
   forall {Idx : Type} (fB : Idx -> set U),
@@ -455,7 +448,21 @@ destruct (HPB2 _ _ HA Hx) as [B HB]; exists B; easy.
 destruct Hx as [B [[HB1 HB2] HB3]]; auto.
 Qed.
 
-Variable PB : set_system U.
+End Basis_Facts1.
+
+
+Section Basis_Facts2.
+
+Context {U : Type}.
+
+Variable T PB : set_system U.
+
+Lemma toto :
+  wFull T -> is_Basisp T PB ->
+  full (unionp_any PB) /\
+  (forall B1 B2 x, exists B3,
+    PB B1 -> PB B2 -> inter B1 B2 x ->
+    PB B3 /\ incl B3 (inter B1 B2) /\ B3 x).
 
 Lemma is_Basisp_Union_any_closure : is_Basisp (Union_any_closure PB) PB.
 Proof.
@@ -463,10 +470,7 @@ split.
 apply Union_any_closure_Gen.
 intros A HA; induction HA as [Q HQ].
 apply set_ext_equiv; split; intros x [B [HB Hx]].
-(* *)
-exists B; repeat split; auto.
-intros y Hy; exists B; easy.
-(* *)
+exists B; repeat split; auto; intros y Hy; exists B; easy.
 destruct HB as [HB1 HB2]; auto.
 Qed.