now

assume I is trivial ; :: thesis: I = {(0. R)}
then consider x being set such that
A1: I = {x} by REALSET1:def 4;
0. R in {x} by A1, Th3;
hence I = {(0. R)} by A1, TARSKI:def 1; :: thesis: verum

end;

hence ( I is trivial iff I = {(0. R)} ) ; :: thesis: verum