for m, n being Nat
for no being Element of OrderedNAT st n = no & m in uparrow no holds
n <= m