let R be Relation of X,Y; :: thesis: R is trivial
A1: ( X is empty or ex x being set st X = {x} ) by ZFMISC_1:131;
A2: ( Y is empty or ex y being set st Y = {y} ) by ZFMISC_1:131;
assume not R is trivial ; :: thesis: contradiction
then consider a1, a2 being set such that
A3: a1 in R and
A4: a2 in R and
A5: a1 <> a2 by ZFMISC_1:def 10;

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 A1, A2;

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

hence contradiction by A3; :: thesis: verum

end;

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

hence contradiction by A3; :: thesis: verum

end;

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

hence contradiction by A3; :: thesis: verum

end;

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

then consider x being set such that
A7: X = {x} ;
consider x1, x2 being set such that
A8: a1 = [x1,x2] and
A9: x1 in X and
A10: x2 in Y by A3, RELSET_1:2;
A11: x1 = x by A7, A9, TARSKI:def 1;
consider y being set such that
A12: Y = {y} by A6;
consider y1, y2 being set such that
A13: a2 = [y1,y2] and
A14: y1 in X and
A15: y2 in Y by A4, RELSET_1:2;
A16: y1 = x by A7, A14, TARSKI:def 1;
x2 = y by A12, A10, TARSKI:def 1;
hence contradiction by A5, A12, A8, A11, A13, A15, A16, TARSKI:def 1; :: thesis: verum

end;

end;