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 ****)
-definition empty_set ≝ λA:Type[0].λa:A.⊥.
+definition empty_set ≝ λA:Type[0].λa:A.False.
notation "\emptyv" non associative with precedence 90 for @{'empty_set}.
interpretation "empty set" 'empty_set = (empty_set ?).
(* 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.