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 set ; :: according to TARSKI:def 3 :: thesis: ( not y in {_{X}_} or y in {_{Y}_} )
assume y in {_{X}_} ; :: thesis: y in {_{Y}_}
then consider x being set such that
A2: ( y = {x} & x in X ) by Th1;
thus y in {_{Y}_} by A1, A2, Th1; :: thesis: verum

end;

assume A3: {_{X}_} c= {_{Y}_} ; :: thesis: X c= Y
let y be set ; :: 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 consider x1 being set such that
A4: ( {y} = {x1} & x1 in Y ) by A3, Th1;
thus y in Y by A4, ZFMISC_1:6; :: thesis: verum