V_______________________________________________________________ *)
include "basics/logic.ma".
+include "basics/core_notation/singl_1.ma".
+include "basics/core_notation/subseteq_2.ma".
(**** a subset of A is just an object of type A→Prop ****)
(* substraction *)
lemma substract_def:∀U.∀A,B:U→Prop. A-B ≐ A ∩ ¬B.
#U #A #B #w normalize /2/
-qed.
\ No newline at end of file
+qed.