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