let x, y be Ordinal; :: thesis: ( x +^ y is natural implies ( x in omega & y in omega ) )
assume A1: x +^ y in omega ; :: according to ORDINAL1:def 13 :: thesis: ( x in omega & y in omega )
( x c= x +^ y & y c= x +^ y ) by Th27;
hence ( x in omega & y in omega ) by A1, ORDINAL1:22; :: thesis: verum