let X1, X2, Y1, Y2 be set ; ( X1 <> {} & Y1 <> {} & [:X1,Y1:] = [:X2,Y2:] implies ( X1 = X2 & Y1 = Y2 ) )
assume A1:
X1 <> {}
; ( not Y1 <> {} or not [:X1,Y1:] = [:X2,Y2:] or ( X1 = X2 & Y1 = Y2 ) )
then consider x being object such that
A2:
x in X1
by XBOOLE_0:7;
assume A3:
Y1 <> {}
; ( not [:X1,Y1:] = [:X2,Y2:] or ( X1 = X2 & Y1 = Y2 ) )
then consider y being object such that
A4:
y in Y1
by XBOOLE_0:7;
assume A5:
[:X1,Y1:] = [:X2,Y2:]
; ( X1 = X2 & Y1 = Y2 )
then A6:
[:X2,Y2:] <> {}
by A1, A3, Th89;
then A7:
Y2 <> {}
by Th89;
for z being object holds
( z in X1 iff z in X2 )
hence
X1 = X2
by TARSKI:2; Y1 = Y2
A9:
X2 <> {}
by A6, Th89;
for z being object holds
( z in Y1 iff z in Y2 )
hence
Y1 = Y2
by TARSKI:2; verum