let n be Nat; :: thesis: ( n is 2 _or_greater implies not n is trivial )
assume n is 2 _or_greater ; :: thesis: not n is trivial
then ( n <> 0 & n <> 1 ) by EC_PF_2:def 1;
hence not n is trivial by NAT_2:def 1; :: thesis: verum