take 1 *^ (exp (omega,1)) ; :: thesis: 1 *^ (exp (omega,1)) is Cantor-component
take 1 ; :: according to ORDINAL5:def 9 :: thesis: ex n being Nat st
( 0 in Segm n & 1 *^ (exp (omega,1)) = n *^ (exp (omega,1)) )
take 1 ; :: thesis: ( 0 in Segm 1 & 1 *^ (exp (omega,1)) = 1 *^ (exp (omega,1)) )
thus ( 0 in Segm 1 & 1 *^ (exp (omega,1)) = 1 *^ (exp (omega,1)) ) by NAT_1:44; :: thesis: verum