let e, X1, Y1, X2, 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 Th123; :: thesis: verum