let R be Relation of X,Y; :: thesis: R is trivial
assume not R is trivial ; :: thesis: contradiction
then consider a1, a2 being set such that
A1: ( a1 in R & a2 in R & a1 <> a2 ) by REALSET1:14;
A2: ( ( X is empty or ex x being set st X = {x} ) & ( Y is empty or ex y being set st Y = {y} ) ) by REALSET1:def 4;

per cases ( ( X is empty & Y is empty ) or ( X is empty & ex x being set st Y = {x} ) or ex x being set st
( X = {x} & Y is empty ) or ex x being set st
( X = {x} & ex y being set st Y = {y} ) ) by A2;

suppose ( X is empty & Y is empty ) ; :: thesis: contradiction

hence contradiction by A1; :: thesis: verum

end;

suppose ( X is empty & ex x being set st Y = {x} ) ; :: thesis: contradiction

hence contradiction by A1; :: thesis: verum

end;

suppose ex x being set st
( X = {x} & Y is empty ) ; :: thesis: contradiction

hence contradiction by A1; :: thesis: verum

end;

suppose A3: ex x being set st
( X = {x} & ex y being set st Y = {y} ) ; :: thesis: contradiction

then consider x being set such that
A4: X = {x} ;
consider y being set such that
A5: Y = {y} by A3;
consider x1, x2 being set such that
A6: ( a1 = [x1,x2] & x1 in X & x2 in Y ) by A1, RELSET_1:6;
A7: ( x1 = x & x2 = y ) by A4, A5, A6, TARSKI:def 1;
consider y1, y2 being set such that
A8: ( a2 = [y1,y2] & y1 in X & y2 in Y ) by A1, RELSET_1:6;
( y1 = x & y2 = y ) by A4, A5, A8, TARSKI:def 1;
hence contradiction by A1, A6, A7, A8; :: thesis: verum

end;

end;