let
X
,
Y
,
Z
be
set
;
:: thesis:
(
X
c=
Y
\/
Z
&
X
misses
Z
implies
X
c=
Y
)
assume
that
A1
:
X
c=
Y
\/
Z
and
A2
:
X
/\
Z
=
{}
;
:: according to
XBOOLE_0:def 7
:: thesis:
X
c=
Y
X
/\
(
Y
\/
Z
)
=
X
by
A1
,
Th28
;
then
(
Y
/\
X
)
\/
{}
=
X
by
A2
,
Th23
;
hence
X
c=
Y
by
Th17
;
:: thesis:
verum