let
A
,
X
,
Y
be
set
;
:: thesis:
(
X
c=
A
&
Y
c=
A
implies
X
\+\
Y
c=
A
)
assume
(
X
c=
A
&
Y
c=
A
) ;
:: thesis:
X
\+\
Y
c=
A
then
(
X
\
Y
c=
A
&
Y
\
X
c=
A
)
by
Th109
;
hence
X
\+\
Y
c=
A
by
Th8
;
:: thesis:
verum