:: deftheorem defines GreaterOrEqualsNumbers NUMBER09:def 5 :
for n being Nat holds GreaterOrEqualsNumbers n = NAT \ (Segm n);