let X, Y be set ; :: thesis: {_{(X \ Y)}_} = {_{X}_} \ {_{Y}_}
thus {_{(X \ Y)}_} c= {_{X}_} \ {_{Y}_} :: according to XBOOLE_0:def 10 :: thesis: {_{X}_} \ {_{Y}_} c= {_{(X \ Y)}_}

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in {_{(X \ Y)}_} or y in {_{X}_} \ {_{Y}_} )
assume y in {_{(X \ Y)}_} ; :: thesis: y in {_{X}_} \ {_{Y}_}
then consider x being set such that
A1: ( y = {x} & x in X \ Y ) by Th1;
A2: ( x in X & not x in Y ) by A1, XBOOLE_0:def 5;
A3: y in {_{X}_} by A1, Th1;
not y in {_{Y}_}

proof

assume y in {_{Y}_} ; :: thesis: contradiction
then consider x1 being set such that
A4: ( y = {x1} & x1 in Y ) by Th1;
thus contradiction by A1, A2, A4, ZFMISC_1:6; :: thesis: verum

end;

hence y in {_{X}_} \ {_{Y}_} by A3, XBOOLE_0:def 5; :: thesis: verum

end;

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in {_{X}_} \ {_{Y}_} or y in {_{(X \ Y)}_} )
assume y in {_{X}_} \ {_{Y}_} ; :: thesis: y in {_{(X \ Y)}_}
then A5: ( y in {_{X}_} & not y in {_{Y}_} ) by XBOOLE_0:def 5;
then consider x being set such that
A6: ( y = {x} & x in X ) by Th1;
not x in Y by A5, A6, Th1;
then x in X \ Y by A6, XBOOLE_0:def 5;
hence y in {_{(X \ Y)}_} by A6, Th1; :: thesis: verum