let X, Y, Z be set ; :: thesis: ( [:(X /\ Y),Z:] = [:X,Z:] /\ [:Y,Z:] & [:Z,(X /\ Y):] = [:Z,X:] /\ [:Z,Y:] )
A1: for x, y being object holds
( [x,y] in [:(X /\ Y),Z:] iff [x,y] in [:X,Z:] /\ [:Y,Z:] )

proof

let x, y be object ; :: thesis: ( [x,y] in [:(X /\ Y),Z:] iff [x,y] in [:X,Z:] /\ [:Y,Z:] )
thus ( [x,y] in [:(X /\ Y),Z:] implies [x,y] in [:X,Z:] /\ [:Y,Z:] ) :: thesis: ( [x,y] in [:X,Z:] /\ [:Y,Z:] implies [x,y] in [:(X /\ Y),Z:] )

proof

assume A2: [x,y] in [:(X /\ Y),Z:] ; :: thesis: [x,y] in [:X,Z:] /\ [:Y,Z:]
then A3: x in X /\ Y by Lm16;
A4: y in Z by A2, Lm16;
x in Y by A3, XBOOLE_0:def 4;
then A5: [x,y] in [:Y,Z:] by A4, Lm16;
x in X by A3, XBOOLE_0:def 4;
then [x,y] in [:X,Z:] by A4, Lm16;
hence [x,y] in [:X,Z:] /\ [:Y,Z:] by A5, XBOOLE_0:def 4; :: thesis: verum

end;

assume A6: [x,y] in [:X,Z:] /\ [:Y,Z:] ; :: thesis: [x,y] in [:(X /\ Y),Z:]
then [x,y] in [:Y,Z:] by XBOOLE_0:def 4;
then A7: x in Y by Lm16;
A8: [x,y] in [:X,Z:] by A6, XBOOLE_0:def 4;
then x in X by Lm16;
then A9: x in X /\ Y by A7, XBOOLE_0:def 4;
y in Z by A8, Lm16;
hence [x,y] in [:(X /\ Y),Z:] by A9, Lm16; :: thesis: verum

end;

[:X,Z:] /\ [:Y,Z:] c= [:X,Z:] by XBOOLE_1:17;
hence A10: [:(X /\ Y),Z:] = [:X,Z:] /\ [:Y,Z:] by A1, Lm17; :: thesis: [:Z,(X /\ Y):] = [:Z,X:] /\ [:Z,Y:]
A11: for y, x being object holds
( [y,x] in [:Z,(X /\ Y):] iff [y,x] in [:Z,X:] /\ [:Z,Y:] )

proof

let y, x be object ; :: thesis: ( [y,x] in [:Z,(X /\ Y):] iff [y,x] in [:Z,X:] /\ [:Z,Y:] )
A12: ( [x,y] in [:X,Z:] & [x,y] in [:Y,Z:] iff ( [y,x] in [:Z,X:] & [y,x] in [:Z,Y:] ) ) by Th87;
( [y,x] in [:Z,(X /\ Y):] iff [x,y] in [:(X /\ Y),Z:] ) by Th87;
hence ( [y,x] in [:Z,(X /\ Y):] iff [y,x] in [:Z,X:] /\ [:Z,Y:] ) by A10, A12, XBOOLE_0:def 4; :: thesis: verum

end;

[:Z,X:] /\ [:Z,Y:] c= [:Z,X:] by XBOOLE_1:17;
hence [:Z,(X /\ Y):] = [:Z,X:] /\ [:Z,Y:] by A11, Lm17; :: thesis: verum