let
A
,
X
,
Y
be
set
;
:: thesis:
(
X
c=
A
implies
X
\
Y
c=
A
)
X
\
Y
c=
X
by
Th36
;
hence
(
X
c=
A
implies
X
\
Y
c=
A
) ;
:: thesis:
verum