let
X
,
Y
be
set
;
:: thesis:
X
\
Y
=
X
\+\
(
X
/\
Y
)
X
/\
Y
c=
X
by
Th17
;
then
(
X
/\
Y
)
\
X
=
{}
by
Lm1
;
hence
X
\
Y
=
X
\+\
(
X
/\
Y
)
by
Th47
;
:: thesis:
verum