theorem Th12: :: CARDFIL4:13

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