let y be object ; :: thesis: for X being set holds
( y in {_{X}_} iff ex x being object st
( y = {x} & x in X ) )
let X be set ; :: thesis: ( y in {_{X}_} iff ex x being object st
( y = {x} & x in X ) )
thus ( y in {_{X}_} implies ex x being object st
( y = {x} & x in X ) ) :: thesis: ( ex x being object st
( y = {x} & x in X ) implies y in {_{X}_} )

proof

assume A1: y in {_{X}_} ; :: thesis: ex x being object st
( y = {x} & x in X )

per cases ( X is empty or not X is empty ) ;

suppose A2: X is empty ; :: thesis: ex x being object st
( y = {x} & x in X )

ex x being object st
( x in X & y = Class ((id X),x) ) by A1, EQREL_1:def 3;
hence ex x being object st
( y = {x} & x in X ) by A2; :: thesis: verum

end;

suppose not X is empty ; :: thesis: ex x being object st
( y = {x} & x in X )

then reconsider X9 = X as non empty set ;
y in { {x} where x is Element of X9 : verum } by A1, EQREL_1:37;
then ex x being Element of X9 st y = {x} ;
hence ex x being object st
( y = {x} & x in X ) ; :: thesis: verum

end;

end;

end;

given x being object such that A3: y = {x} and
A4: x in X ; :: thesis: y in {_{X}_}
reconsider X9 = X as non empty set by A4;
y in { {z} where z is Element of X9 : verum } by A3, A4;
hence y in {_{X}_} by EQREL_1:37; :: thesis: verum