take A = <%(1 *^ (exp (omega,1)))%>; :: thesis: ( not A is empty & A is Cantor-normal-form )
thus not A is empty ; :: thesis: A is Cantor-normal-form
0 in Segm 1 by NAT_1:44;
hence A is Cantor-normal-form by Th65; :: thesis: verum