definition subset: ∀A:Type[0].∀P,Q:A→Prop.Prop ≝ λA,P,Q.∀a:A.(P a → Q a).
interpretation "subset" 'subseteq a b = (subset ? a b).
-(* \ 5h2 class="section"\ 6Set Quality\ 5/h2\ 6
+(*
+\ 5h2 class="section"\ 6Set Equality\ 5/h2\ 6
Two sets are equals if and only if they have the same elements, that is,
if the two characteristic functions are extensionally equivalent: *)
B \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61 C → A \ 5a title="substraction" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6 B \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61 A \ 5a title="substraction" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6 C.
#U #A #B #C #eqBC #a @\ 5a href="cic:/matita/basics/logic/iff_and_l.def(2)"\ 6iff_and_l\ 5/a\ 6 /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/iff_not.def(4)"\ 6iff_not\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ qed.
-(* We can now prove several properties of the previous set-theoretic operations.
+(*
+\ 5h2 class="section"\ 6Simple properties of sets\ 5/h2\ 6
+We can now prove several properties of the previous set-theoretic operations.
In particular, union is commutative and associative, and the empty set is an
identity element: *)