:: deftheorem Def1 defines trivial NAT_2:def 1 :
for n being Nat holds
( n is trivial iff ( n = 0 or n = 1 ) );