let
X
,
Y
be
set
;
:: thesis:
X
/\
Y
misses
X
\+\
Y
(
X
/\
Y
misses
X
\
Y
&
X
/\
Y
misses
Y
\
X
)
by
Th89
;
hence
X
/\
Y
misses
X
\+\
Y
by
Th70
;
:: thesis:
verum