let
x
be
object
;
:: according to
VALUED_2:def 4
:: thesis:
( not
x
in
()
X
or
x
is
set
)
assume
A1
:
x
in
()
X
;
:: thesis:
x
is
set
then
reconsider
x
=
x
as
Element
of
()
X
;
A2
:

x
in
X
by
A1
,
Th24
;
(

(

x
)
=
x
&
()
(
()
X
)
=
X
) ;
hence
x
is
set
by
A2
;
:: thesis:
verum