let A, B be Ordinal; :: thesis: ( not A *^ B = {} or A = {} or B = {} )
assume A1: ( A *^ B = {} & A <> {} & B <> {} ) ; :: thesis: contradiction
{} c= A by XBOOLE_1:2;
then {} c< A by A1, XBOOLE_0:def 8;
hence contradiction by A1, ORDINAL1:21, ORDINAL2:57; :: thesis: verum