:: deftheorem Def0 defines trivial NEWTON03:def 1 :
for a being Nat holds
( a is trivial iff a <= 1 );