let X1, X2, Y1, Y2 be set ; :: thesis: ( [:X1,X2:] c= [:Y1,Y2:] & [:X1,X2:] <> {} implies ( X1 c= Y1 & X2 c= Y2 ) )
assume that
A1: [:X1,X2:] c= [:Y1,Y2:] and
A2: [:X1,X2:] <> {} ; :: thesis: ( X1 c= Y1 & X2 c= Y2 )
A3: [:X1,X2:] = [:X1,X2:] /\ [:Y1,Y2:] by A1, XBOOLE_1:28
.= [:(X1 /\ Y1),(X2 /\ Y2):] by Th99 ;
( X1 <> {} & X2 <> {} ) by A2, Th89;
then ( X1 = X1 /\ Y1 & X2 = X2 /\ Y2 ) by A3, Th109;
hence ( X1 c= Y1 & X2 c= Y2 ) by XBOOLE_1:17; :: thesis: verum