now :: thesis: ( I is trivial implies I = {(0. R)} )
assume I is trivial ; :: thesis: I = {(0. R)}
then consider x being object such that
A1: I = {x} by ZFMISC_1:131;
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