let
X
,
Y
be
set
;
:: thesis:
X
\/
Y
=
(
X
\+\
Y
)
\+\
(
X
/\
Y
)
X
/\
Y
misses
X
\+\
Y
by
Lm4
;
then
(
(
X
\+\
Y
)
\
(
X
/\
Y
)
=
X
\+\
Y
&
(
X
/\
Y
)
\
(
X
\+\
Y
)
=
X
/\
Y
)
by
Th83
;
hence
X
\/
Y
=
(
X
\+\
Y
)
\+\
(
X
/\
Y
)
by
Th93
;
:: thesis:
verum