consider
x
being
object
such that
A1
:
x
in
X
by
XBOOLE_0:def 1
;
reconsider
x
=
x
as
Element
of
X
by
A1
;

x
in
()
X
by
Def3
;
hence
not
()
X
is
empty
;
:: thesis:
verum