let x, y be Ordinal; ( x *^ y is natural & not x *^ y is empty implies ( x in omega & y in omega ) )
assume A1:
x *^ y in omega
; ORDINAL1:def 12 ( x *^ y is empty or ( x in omega & y in omega ) )
assume A2:
not x *^ y is empty
; ( x in omega & y in omega )
then
y <> {}
by ORDINAL2:38;
then A3:
x c= x *^ y
by Th36;
x <> {}
by A2, ORDINAL2:35;
then
y c= x *^ y
by Th36;
hence
( x in omega & y in omega )
by A1, A3, ORDINAL1:12; verum