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;
( x in X or x in Y ) by A1, 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 set ; :: according to TARSKI:def 3 :: thesis: ( not y in {_{X}_} \/ {_{Y}_} or y in {_{(X \/ Y)}_} )
assume A2: y in {_{X}_} \/ {_{Y}_} ; :: thesis: y in {_{(X \/ Y)}_}

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

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

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

end;

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

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

end;

end;