:: deftheorem Def1 defines _or_greater EC_PF_2:def 1 :
for n, p being Real holds
( p is n _or_greater iff n <= p );