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:55;
{} c= B by XBOOLE_1:2;
then {} c< B by A2, XBOOLE_0:def 8;
then {} in B by ORDINAL1:21;
then A3: 1 c= B by Lm1, ORDINAL1:33;

A4: now

assume A in 1 ; :: thesis: contradiction
then A c= {} by Lm1, ORDINAL1:34;
then A = {} by XBOOLE_1:3;
hence contradiction by A1, ORDINAL2:52; :: thesis: verum

end;

now

assume 1 in A ; :: thesis: contradiction
then ( 1 *^ B in A *^ B & B = 1 *^ B ) by A2, ORDINAL2:56, ORDINAL2:57;
hence contradiction by A1, A3, ORDINAL1:7; :: thesis: verum

end;

hence A = 1 by A4, ORDINAL1:24; :: thesis: B = 1
hence B = 1 by A1, ORDINAL2:56; :: thesis: verum