let n be natural number ; :: thesis: ( not n is trivial & n is odd implies n is 2 _greater )
assume A2: ( not n is trivial & n is odd ) ; :: thesis: n is 2 _greater
( n <= 2 implies not not n = 0 & ... & not n = 2 ) ;
hence n is 2 _greater by A2; :: thesis: verum