let
X
,
Y
,
Z
be
set
;
:: thesis:
(
X
misses
Y
\
Z
implies
Y
misses
X
\
Z
)
X
/\
(
Y
\
Z
)
=
(
Y
/\
X
)
\
Z
by
Th49
.=
Y
/\
(
X
\
Z
)
by
Th49
;
hence
(
X
misses
Y
\
Z
implies
Y
misses
X
\
Z
) ;
:: thesis:
verum