let X1, X2, Y1, 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 object 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 object such that
A4: y in Y1 by XBOOLE_0:7;
assume A5: [:X1,Y1:] = [:X2,Y2:] ; :: thesis: ( 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 )
proof
let z be object ; :: thesis: ( z in X1 iff z in X2 )
consider y2 being object such that
A8: y2 in Y2 by A7, XBOOLE_0:7;
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, Lm16;
hence z in X2 by Lm16; :: thesis: verum
end;
assume z in X2 ; :: thesis: z in X1
then [z,y2] in [:X2,Y2:] by A8, Lm16;
hence z in X1 by A5, Lm16; :: thesis: verum
end;
hence X1 = X2 by TARSKI:2; :: thesis: Y1 = Y2
A9: X2 <> {} by A6, Th89;
for z being object holds
( z in Y1 iff z in Y2 )
proof
let z be object ; :: thesis: ( z in Y1 iff z in Y2 )
consider x2 being object such that
A10: x2 in X2 by A9, XBOOLE_0:7;
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, Lm16;
hence z in Y2 by Lm16; :: thesis: verum
end;
assume z in Y2 ; :: thesis: z in Y1
then [x2,z] in [:X2,Y2:] by A10, Lm16;
hence z in Y1 by A5, Lm16; :: thesis: verum
end;
hence Y1 = Y2 by TARSKI:2; :: thesis: verum