let
X
,
Y
be
set
;
:: thesis:
(
X
misses
Y
implies
(
X
\/
Y
)
\
Y
=
X
)
assume
A1
:
X
misses
Y
;
:: thesis:
(
X
\/
Y
)
\
Y
=
X
thus
(
X
\/
Y
)
\
Y
=
(
X
\
Y
)
\/
(
Y
\
Y
)
by
Th42
.=
(
X
\
Y
)
\/
{}
by
Lm1
.=
X
by
A1
,
Th83
;
:: thesis:
verum