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

proof

assume A1: y in {_{X}_} ; :: thesis: ex x being set 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 set st
( y = {x} & x in X )

consider x being set such that
A3: ( x in X & y = Class (id X),x ) by A1, EQREL_1:def 5;
thus ex x being set st
( y = {x} & x in X ) by A2, A3; :: thesis: verum

end;

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

then reconsider X' = X as non empty set ;
y in { {x} where x is Element of X' : verum } by A1, EQREL_1:46;
then consider x being Element of X' such that
A4: y = {x} ;
thus ex x being set st
( y = {x} & x in X ) by A4; :: thesis: verum

end;

end;

end;

given x being set such that A5: ( y = {x} & x in X ) ; :: thesis: y in {_{X}_}
reconsider X' = X as non empty set by A5;
y in { {z} where z is Element of X' : verum } by A5;
hence y in {_{X}_} by EQREL_1:46; :: thesis: verum