let
X
,
Y
,
Z
be
set
;
:: thesis:
(
X
c=
Y
implies
X
misses
Z
\
Y
)
assume
A1
:
X
c=
Y
;
:: thesis:
X
misses
Z
\
Y
thus
X
/\
(
Z
\
Y
)
=
(
Z
/\
X
)
\
Y
by
Th49
.=
Z
/\
(
X
\
Y
)
by
Th49
.=
Z
/\
{}
by
A1
,
Lm1
.=
{}
;
:: according to
XBOOLE_0:def 7
:: thesis:
verum