let
X
,
Y
be
set
;
:: thesis:
X
\/
Y
=
X
\+\
(
Y
\
X
)
A1
:
(
Y
\
X
)
\
X
=
Y
\
(
X
\/
X
)
by
Th41
.=
Y
\
X
;
X
\
(
Y
\
X
)
=
(
X
\
Y
)
\/
(
X
/\
X
)
by
Th52
.=
X
by
Th12
,
Th36
;
hence
X
\/
Y
=
X
\+\
(
Y
\
X
)
by
A1
,
Th39
;
:: thesis:
verum