for a, b being Ordinal st a +^ b is natural holds
( a in omega & b in omega ) by Th24, ORDINAL1:12;