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 12 :: thesis: ( x in omega & y in omega )
A2: y c= x +^ y by Th27;
x c= x +^ y by Th27;
hence ( x in omega & y in omega ) by A1, A2, ORDINAL1:12; :: thesis: verum