assume
not
()
X
is
empty
;
:: thesis:
contradiction
then
consider
x
being
object
such that
A1
:
x
in
()
X
;
reconsider
x
=
x
as
Element
of
()
X
by
A1
;

(

x
)
=
x
;
hence
contradiction
by
A1
,
Def3
;
:: thesis:
verum