let k be Element of GreaterOrEqualsNumbers n; :: thesis: k is n _or_greater
thus n <= k by Th56; :: according to EC_PF_2:def 1 :: thesis: verum