:: deftheorem Def2 defines trivial FIELD_3:def 2 :
for R being Ring
for a being Element of R holds
( a is trivial iff ( a = 1. R or a = 0. R ) );