let n be Nat; :: thesis: ( n is 4 _or_greater implies ( n is 3 _or_greater & not n is zero ) )
assume n is 4 _or_greater ; :: thesis: ( n is 3 _or_greater & not n is zero )
then n >= 4 by EC_PF_2:def 1;
hence ( n is 3 _or_greater & not n is zero ) by EC_PF_2:def 1, XXREAL_0:2; :: thesis: verum