let X1, X2, Y1, Y2 be set ; ( [: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:] <> {}
; ( 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; verum