let X, Y be set ; :: thesis: ( X <> {} & Y <> {} & [:X,Y:] = [:Y,X:] implies X = Y )
assume X <> {} ; :: thesis: ( not Y <> {} or not [:X,Y:] = [:Y,X:] or X = Y )
then consider x being object such that
A1: x in X by XBOOLE_0:7;
assume Y <> {} ; :: thesis: ( not [:X,Y:] = [:Y,X:] or X = Y )
then consider y being object such that
A2: y in Y by XBOOLE_0:7;
assume A3: [:X,Y:] = [:Y,X:] ; :: thesis: X = Y
for z being object holds
( z in X iff z in Y )
proof
let z be object ; :: thesis: ( z in X iff z in Y )
thus ( z in X implies z in Y ) :: thesis: ( z in Y implies z in X )
proof
assume z in X ; :: thesis: z in Y
then [z,y] in [:Y,X:] by A2, A3, Lm16;
hence z in Y by Lm16; :: thesis: verum
end;
assume z in Y ; :: thesis: z in X
then [z,x] in [:X,Y:] by A1, A3, Lm16;
hence z in X by Lm16; :: thesis: verum
end;
hence X = Y by TARSKI:2; :: thesis: verum