Renaming (Inter_with_empty -> Inter_wEmpty).

Add results about Inter and Union when adding {empty,full}set.

Lebesgue/Set_theory/Set_system/Set_system_base_base.v

@@ -210,8 +210,8 @@ Proof.
 intros H A B _ HA HB; now apply H.
 Qed.
 
-Lemma Inter_with_empty :
-  Inter P -> Inter (fun A => P A \/ A = emptyset).
+Lemma Inter_wEmpty :
+  Inter P -> Inter (add P emptyset).
 Proof.
 intros H A B [HA | HA] [HB | HB].
 left; now apply H.
@@ -219,6 +219,16 @@ right; rewrite HB; apply inter_emptyset_r.
 1,2: right; rewrite HA; apply inter_emptyset_l.
 Qed.
 
+Lemma Inter_wFull :
+  Inter P -> Inter (add P fullset).
+Proof.
+intros H A B [HA | HA] [HB | HB].
+left; now apply H.
+left; now rewrite HB, inter_fullset_r.
+left; now rewrite HA, inter_fullset_l.
+right; now rewrite HA, HB, inter_fullset_l.
+Qed.
+
 Lemma Inter_Diff :
   Compl P -> Inter P -> Diff P.
 Proof.
@@ -263,6 +273,25 @@ now apply Inter_Diff.
 apply Diff_Inter.
 Qed.
 
+Lemma Union_wEmpty :
+  Union P -> Union (add P emptyset).
+Proof.
+intros H A B [HA | HA] [HB | HB].
+left; now apply H.
+left; now rewrite HB, union_emptyset_r.
+left; now rewrite HA, union_emptyset_l.
+right; now rewrite HA, HB, union_emptyset_l.
+Qed.
+
+Lemma Union_wFull :
+  Union P -> Union (add P fullset).
+Proof.
+intros H A B [HA | HA] [HB | HB].
+left; now apply H.
+right; rewrite HB; apply union_fullset_r.
+1,2: right; rewrite HA; apply union_fullset_l.
+Qed.
+
 Lemma Union_disj_Union :
   Diff P -> Union_disj P -> Union P.
 Proof.