let X1, X2, Y1, Y2 be set ; :: thesis: [:(X1 /\ X2),(Y1 /\ Y2):] = [:X1,Y1:] /\ [:X2,Y2:]
( Y1 /\ Y2 c= Y2 & X1 /\ X2 c= X2 ) by XBOOLE_1:17;
then A1: [:(X1 /\ X2),(Y1 /\ Y2):] c= [:X2,Y2:] by Th95;
A2: [:X1,Y1:] /\ [:X2,Y2:] c= [:(X1 /\ X2),(Y1 /\ Y2):]
proof
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in [:X1,Y1:] /\ [:X2,Y2:] or z in [:(X1 /\ X2),(Y1 /\ Y2):] )
assume z in [:X1,Y1:] /\ [:X2,Y2:] ; :: thesis: z in [:(X1 /\ X2),(Y1 /\ Y2):]
then ex x, y being object st
( z = [x,y] & x in X1 /\ X2 & y in Y1 /\ Y2 ) by Th84;
hence z in [:(X1 /\ X2),(Y1 /\ Y2):] by Def2; :: thesis: verum
end;
( Y1 /\ Y2 c= Y1 & X1 /\ X2 c= X1 ) by XBOOLE_1:17;
then [:(X1 /\ X2),(Y1 /\ Y2):] c= [:X1,Y1:] by Th95;
hence [:(X1 /\ X2),(Y1 /\ Y2):] = [:X1,Y1:] /\ [:X2,Y2:] by A2, A1, XBOOLE_1:19; :: thesis: verum