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).
-(* Two sets are equals if and only if they have the same elements, that is,
+(*
+\ 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: *)
definition eqP ≝ λA:Type[0].λP,Q:A → Prop.∀a:A.P a \ 5a title="iff" href="cic:/fakeuri.def(1)"\ 6↔\ 5/a\ 6\ 5span class="error" title="Parse error: [term] expected after [sym↔] (in [term])"\ 6\ 5/span\ 6 Q a.
notation "A =1 B" non associative with precedence 45 for @{'eqP $A $B}.
interpretation "extensional equality" 'eqP a b = (eqP ? a b).
-(* This notion of equality is different from the intensional equality of
+(*
+This notion of equality is different from the intensional equality of
functions; the fact it defines an equivalence relation must be explicitly
proved: *)
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: *)