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

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume y in {_{(X \/ Y)}_} ; :: thesis:
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:

end;

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

per cases by A3, XBOOLE_0:def 3;

suppose y in {_{X}_} ; :: thesis:

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:

end;

suppose y in {_{Y}_} ; :: thesis:

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:

end;

end;