let a be ordinal number ; :: thesis: ( a is Cantor-component implies not a is empty )
given b being ordinal number , n being natural number such that A1: ( 0 in n & a = n *^ (exp (omega,b)) ) ; :: according to ORDINAL5:def 9 :: thesis: not a is empty
exp (omega,b) <> 0 by ORDINAL4:22;
hence not a is empty by A1, ORDINAL3:31; :: thesis: verum