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;
( x in X or x in Y ) by A2, XBOOLE_0:def 3;
then ( y in {_{X}_} or y in {_{Y}_} ) by A1, Th1;
hence y in {_{X}_} \/ {_{Y}_} by XBOOLE_0:def 3; :: thesis: verum

end;

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in {_{X}_} \/ {_{Y}_} or y in {_{(X \/ Y)}_} )
assume A3: y in {_{X}_} \/ {_{Y}_} ; :: thesis: y in {_{(X \/ Y)}_}

per cases ( y in {_{X}_} or y in {_{Y}_} ) by A3, XBOOLE_0:def 3;

suppose y in {_{X}_} ; :: thesis: y in {_{(X \/ Y)}_}

then consider x being object such that
A4: y = {x} and
A5: x in X by Th1;
x in X \/ Y by A5, XBOOLE_0:def 3;
hence y in {_{(X \/ Y)}_} by A4, Th1; :: thesis: verum

end;

suppose y in {_{Y}_} ; :: thesis: y in {_{(X \/ Y)}_}

then consider x being object such that
A6: y = {x} and
A7: x in Y by Th1;
x in X \/ Y by A7, XBOOLE_0:def 3;
hence y in {_{(X \/ Y)}_} by A6, Th1; :: thesis: verum

end;

end;