let A, B be Ordinal; :: thesis: ( not A *^ B = {} or A = {} or B = {} )
assume that
A1: A *^ B = {} and
A2: A <> {} and
A3: B <> {} ; :: thesis: contradiction
{} c= A ;
then {} c< A by A2;
hence contradiction by A1, A3, ORDINAL1:11, ORDINAL2:40; :: thesis: verum