take n ; :: thesis: ( n is n _or_greater & not n is zero )
thus ( n is n _or_greater & not n is zero ) by EC_PF_2:def 1; :: thesis: verum