theorem Th13: :: CARDFIL4:14

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