for n being Nat
for no being Element of OrderedNAT st n = no holds
uparrow no = NAT \ (Segm n)