let X, Y be set ; :: thesis: ( X c= Y iff {_{X}_} c= {_{Y}_} )
thus ( X c= Y implies {_{X}_} c= {_{Y}_} ) :: thesis: ( {_{X}_} c= {_{Y}_} implies X c= Y )

proof

assume A1: X c= Y ; :: thesis: {_{X}_} c= {_{Y}_}
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in {_{X}_} or y in {_{Y}_} )
assume y in {_{X}_} ; :: thesis: y in {_{Y}_}
then ex x being object st
( y = {x} & x in X ) by Th1;
hence y in {_{Y}_} by A1, Th1; :: thesis: verum

end;

assume A2: {_{X}_} c= {_{Y}_} ; :: thesis: X c= Y
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in X or y in Y )
assume y in X ; :: thesis: y in Y
then {y} in {_{X}_} by Th1;
then ex x1 being object st
( {y} = {x1} & x1 in Y ) by A2, Th1;
hence y in Y by ZFMISC_1:3; :: thesis: verum