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

proof

let z be set ; :: thesis: ( z in X1 iff z in X2 )
thus ( z in X1 implies z in X2 ) :: thesis: ( z in X2 implies z in X1 )

proof

assume z in X1 ; :: thesis: z in X2
then [z,y] in [:X2,Y2:] by A4, A5, Lm17;
hence z in X2 by Lm17; :: thesis: verum

end;

consider y2 being set such that
A7: y2 in Y2 by A6, XBOOLE_0:7;
assume z in X2 ; :: thesis: z in X1
then [z,y2] in [:X2,Y2:] by A7, Lm17;
hence z in X1 by A5, Lm17; :: thesis: verum

end;

hence X1 = X2 by TARSKI:2; :: thesis: Y1 = Y2
for z being set holds
( z in Y1 iff z in Y2 )

proof

let z be set ; :: thesis: ( z in Y1 iff z in Y2 )
thus ( z in Y1 implies z in Y2 ) :: thesis: ( z in Y2 implies z in Y1 )

proof

assume z in Y1 ; :: thesis: z in Y2
then [x,z] in [:X2,Y2:] by A2, A5, Lm17;
hence z in Y2 by Lm17; :: thesis: verum

end;

consider x2 being set such that
A8: x2 in X2 by A6, XBOOLE_0:7;
assume z in Y2 ; :: thesis: z in Y1
then [x2,z] in [:X2,Y2:] by A8, Lm17;
hence z in Y1 by A5, Lm17; :: thesis: verum

end;

hence Y1 = Y2 by TARSKI:2; :: thesis: verum