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 13 ( 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:55;
then A3:
x c= x *^ y
by Th39;
x <> {}
by A2, ORDINAL2:52;
then
y c= x *^ y
by Th39;
hence
( x in omega & y in omega )
by A1, A3, ORDINAL1:22; verum