theorem :: ORDINAL3:75

for a, b being Ordinal st a *^ b is natural & not a *^ b is empty holds
( a in omega & b in omega )