let
X
,
Y
,
Z
be
set
;
:: thesis:
(
Y
misses
Z
implies
X
/\
Y
misses
X
/\
Z
)
assume
Y
misses
Z
;
:: thesis:
X
/\
Y
misses
X
/\
Z
then
X
/\
Z
misses
Y
by
Th74
;
hence
X
/\
Y
misses
X
/\
Z
by
Th74
;
:: thesis:
verum