theorem :: ORDINAL7:23
for c, d, e being Cantor-component Ordinal st omega -exponent d in omega -exponent c & omega -exponent e in omega -exponent d holds
<%c,d,e%> is Cantor-normal-form