take n ; :: thesis: n is n _or_greater
thus n <= n ; :: according to EC_PF_2:def 1 :: thesis: verum