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