take n ; :: thesis: n is n _or_greater
thus n is n _or_greater by EC_PF_2:def 1; :: thesis: verum