Proof of is_Basisp_equiv.

Lebesgue/Set_theory/Set_system/Set_system_any.v

@@ -404,11 +404,11 @@ intros Idx fB; split; intros [HfB1 HfB2]; split.
 intros B [i]; easy.
 intros A HA; rewrite (HfB2 A HA) at 1; apply set_ext_equiv; split; intros x.
 intros [i [Hx1 Hx2]]; exists (fB i); easy.
-intros [B [[HB1 HB2] Hx]]; induction HB2 as [i]; exists i; easy.
+intros [B [[HB1 HB2] Hx]]; induction HB1 as [i]; exists i; easy.
 (* *)
 intros; apply HfB1; easy.
 intros A HA; rewrite (HfB2 A HA) at 1; apply set_ext_equiv; split; intros x.
-intros [B [[HB1 HB2] Hx]]; induction HB2 as [i]; exists i; easy.
+intros [B [[HB1 HB2] Hx]]; induction HB1 as [i]; exists i; easy.
 intros [i [Hx1 Hx2]]; exists (fB i); easy.
 Qed.
 
@@ -431,15 +431,15 @@ Variable T : set_system U.
 Lemma is_Basisp_equiv :
   forall (PB : set_system U),
     is_Basisp T PB <->
-    (forall A x, T A -> A x -> exists B, PB B /\ incl B A /\ B x).
+    (Incl PB T /\ forall A x, T A -> A x -> exists B, PB B /\ incl B A /\ B x).
 Proof.
-intros PB; split.
-(* *)
-intros [HPB1 HPB2] A x HA Hx.
-
-
-
-Admitted.
+intros PB; split; intros [HPB1 HPB2]; split; try easy.
+intros A x HA Hx; rewrite (HPB2 _ HA) in Hx;
+    destruct Hx as [B HB]; exists B; easy.
+intros A HA; apply set_ext_equiv; split; intros x Hx.
+destruct (HPB2 _ _ HA Hx) as [B HB]; exists B; easy.
+destruct Hx as [B [[HB1 HB2] HB3]]; auto.
+Qed.
 
 Variable P : set_system U.