let e be object ; :: thesis: for X1, X2, Y1, Y2 being set st e in [:X1,Y1:] & e in [:X2,Y2:] holds
e in [:(X1 /\ X2),(Y1 /\ Y2):]
let X1, X2, Y1, Y2 be set ; :: thesis: ( e in [:X1,Y1:] & e in [:X2,Y2:] implies e in [:(X1 /\ X2),(Y1 /\ Y2):] )
assume ( e in [:X1,Y1:] & e in [:X2,Y2:] ) ; :: thesis: e in [:(X1 /\ X2),(Y1 /\ Y2):]
then e in [:X1,Y1:] /\ [:X2,Y2:] by XBOOLE_0:def 4;
hence e in [:(X1 /\ X2),(Y1 /\ Y2):] by Th99; :: thesis: verum