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 1 by NAT_1:45;
hence A is Cantor-normal-form by Th44; :: thesis: verum