let a be Ordinal; :: thesis: ( a is Cantor-component implies not a is empty )
given b being Ordinal, n being Nat such that A1: ( 0 in Segm 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