let R be Relation; :: thesis: ( R is trivial implies dom R is trivial )
assume A1: R is trivial ; :: thesis: dom R is trivial

per cases ( R is empty or ex x being set st R = {x} ) by A1, REALSET1:def 4;

suppose R is empty ; :: thesis: dom R is trivial

hence dom R is trivial by RELAT_1:60; :: thesis: verum

end;

suppose ex x being set st R = {x} ; :: thesis: dom R is trivial

then consider x being set such that
A2: R = {x} ;
x in R by A2, TARSKI:def 1;
then consider y being set such that
A3: ex z being set st x = [y,z] by RELAT_1:def 1;
thus dom R is trivial by A2, A3, RELAT_1:23; :: thesis: verum

end;

end;