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: x in X by A2, XBOOLE_0:def 4;
A4: x in Y by A2, XBOOLE_0:def 4;
A5: y in {_{X}_} by A1, A3, Th1;
y in {_{Y}_} by A1, A4, Th1;
hence y in {_{X}_} /\ {_{Y}_} by A5, XBOOLE_0:def 4; :: thesis: verum
end;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in {_{X}_} /\ {_{Y}_} or y in {_{(X /\ Y)}_} )
assume A6: y in {_{X}_} /\ {_{Y}_} ; :: thesis: y in {_{(X /\ Y)}_}
then A7: y in {_{X}_} by XBOOLE_0:def 4;
A8: y in {_{Y}_} by A6, XBOOLE_0:def 4;
consider x being object such that
A9: y = {x} and
A10: x in X by A7, Th1;
consider x1 being object such that
A11: y = {x1} and
A12: x1 in Y by A8, Th1;
x = x1 by A9, A11, ZFMISC_1:3;
then x in X /\ Y by A10, A12, XBOOLE_0:def 4;
hence y in {_{(X /\ Y)}_} by A9, Th1; :: thesis: verum