let A, B be Ordinal; :: thesis: ( A *^ B = 1 implies ( A = 1 & B = 1 ) )
assume A1: A *^ B = 1 ; :: thesis: ( A = 1 & B = 1 )
then A2: B <> {} by ORDINAL2:38;
{} c= B ;
then {} c< B by A2;
then {} in B by ORDINAL1:11;
then A3: 1 c= B by Lm1, ORDINAL1:21;
A4: now :: thesis: not 1 in A
A5: B = 1 *^ B by ORDINAL2:39;
assume 1 in A ; :: thesis: contradiction
hence contradiction by A1, A2, A3, A5, ORDINAL1:5, ORDINAL2:40; :: thesis: verum
end;
now :: thesis: not A in 1
assume A in 1 ; :: thesis: contradiction
then A c= {} by Lm1, ORDINAL1:22;
then A = {} by XBOOLE_1:3;
hence contradiction by A1, ORDINAL2:35; :: thesis: verum
end;
hence A = 1 by A4, ORDINAL1:14; :: thesis: B = 1
hence B = 1 by A1, ORDINAL2:39; :: thesis: verum