theorem Th71: :: ORDINAL7:58

for n being non zero Nat holds CantorNF n = <%n%>