S
c=
X
by
PBOOLE:def 18
;
then
(
z
in
S
.
x
&
S
.
x
c=
X
.
x
& not
S
.
x
is
empty
) ;
hence
z
is
Element
of
X
.
x
;
:: thesis:
verum