+lemma eqP_intersect_r: ∀U.∀A,B,C:U →Prop.
+ A ≐ C → A ∩ B ≐ C ∩ B.
+#U #A #B #C #eqAB #a @iff_and_r @eqAB qed.
+
+lemma eqP_intersect_l: ∀U.∀A,B,C:U →Prop.
+ B ≐ C → A ∩ B ≐ A ∩ C.
+#U #A #B #C #eqBC #a @iff_and_l @eqBC qed.
+
+lemma eqP_substract_r: ∀U.∀A,B,C:U →Prop.
+ A ≐ C → A - B ≐ C - B.
+#U #A #B #C #eqAB #a @iff_and_r @eqAB qed.
+
+lemma eqP_substract_l: ∀U.∀A,B,C:U →Prop.
+ B ≐ C → A - B ≐ A - C.
+#U #A #B #C #eqBC #a @iff_and_l /2/ qed.
+