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 A0: ( 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 A0, ORDINAL3:34; :: thesis: verum