let
X
,
Y
be
set
;
:: thesis:
X
\/
Y
=
(
X
\+\
Y
)
\/
(
X
/\
Y
)
thus
X
\/
Y
=
(
(
X
\
Y
)
\/
(
X
/\
Y
)
)
\/
Y
by
Th51
.=
(
X
\
Y
)
\/
(
(
X
/\
Y
)
\/
Y
)
by
Th4
.=
(
X
\
Y
)
\/
Y
by
Th22
.=
(
X
\
Y
)
\/
(
(
Y
\
X
)
\/
(
Y
/\
X
)
)
by
Th51
.=
(
X
\+\
Y
)
\/
(
X
/\
Y
)
by
Th4
;
:: thesis:
verum