let a be Cantor-component Ordinal; :: thesis: CantorNF a = <%a%>
Sum^ <%a%> = a by ORDINAL5:53;
hence CantorNF a = <%a%> ; :: thesis: verum