let n be natural number ; :: thesis: ( not n is trivial implies n is 2 _or_greater )
assume A1: not n is trivial ; :: thesis: n is 2 _or_greater
( n <= 1 implies not not n = 0 & ... & not n = 1 ) ;
then n >= 1 + 1 by A1, NAT_1:13;
hence n is 2 _or_greater ; :: thesis: verum