let
X
,
Y
be
set
;
:: thesis:
X
\/
(
X
\/
Y
)
=
X
\/
Y
X
\/
(
X
\/
Y
)
=
(
X
\/
X
)
\/
Y
by
Th4
.=
X
\/
Y
;
hence
X
\/
(
X
\/
Y
)
=
X
\/
Y
;
:: thesis:
verum