let
X
,
Y
be
set
;
:: thesis:
X
/\
Y
=
(
X
\+\
Y
)
\+\
(
X
\/
Y
)
X
\+\
Y
=
(
X
\/
Y
)
\
(
X
/\
Y
)
by
Lm5
;
then
X
\+\
Y
c=
X
\/
Y
by
Th36
;
then
A1
:
(
X
\+\
Y
)
\
(
X
\/
Y
)
=
{}
by
Lm1
;
X
\/
Y
=
(
X
\+\
Y
)
\/
(
X
/\
Y
)
by
Th93
;
hence
X
/\
Y
=
(
X
\+\
Y
)
\+\
(
X
\/
Y
)
by
A1
,
Lm4
,
Th88
;
:: thesis:
verum