:: deftheorem Def9 defines Cantor-component ORDINAL5:def 9 :
for a being Ordinal holds
( a is Cantor-component iff ex b being Ordinal ex n being Nat st
( 0 in Segm n & a = n *^ (exp (omega,b)) ) );