let x, y be Ordinal; :: thesis: ( x *^ y is natural & not x *^ y is empty implies ( x in omega & y in omega ) )
assume A1: x *^ y in omega ; :: according to ORDINAL1:def 13 :: thesis: ( x *^ y is empty or ( x in omega & y in omega ) )
assume not x *^ y is empty ; :: thesis: ( x in omega & y in omega )
then ( x <> {} & y <> {} ) by ORDINAL2:52, ORDINAL2:55;
then ( x c= x *^ y & y c= x *^ y ) by Th39;
hence ( x in omega & y in omega ) by A1, ORDINAL1:22; :: thesis: verum