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 object ; :: 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 object such that
A1: y = {x} and
A2: x in X \ Y by Th1;
A3: not x in Y by A2, XBOOLE_0:def 5;
A4: y in {_{X}_} by A1, A2, Th1;
not y in {_{Y}_}

proof

assume y in {_{Y}_} ; :: thesis: contradiction
then ex x1 being object st
( y = {x1} & x1 in Y ) by Th1;
hence contradiction by A1, A3, ZFMISC_1:3; :: thesis: verum

end;

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

end;

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