:: deftheorem Def4 defines CantorNF ORDINAL7:def 4 :
for a being Ordinal
for b₂ being Cantor-normal-form Ordinal-Sequence holds
( b₂ = CantorNF a iff Sum^ b₂ = a );