let A, B, C be Ordinal; :: thesis: ( A in B & C <> {} implies ( A in B *^ C & A in C *^ B ) )
assume A1: ( A in B & C <> {} ) ; :: thesis: ( A in B *^ C & A in C *^ B )
{} c= C by XBOOLE_1:2;
then {} c< C by A1, XBOOLE_0:def 8;
then {} in C by ORDINAL1:21;
then 1 c= C by Lm1, ORDINAL1:33;
then ( B *^ 1 c= B *^ C & 1 *^ B c= C *^ B & B *^ 1 = B & 1 *^ B = B ) by ORDINAL2:56, ORDINAL2:58, ORDINAL2:59;
hence ( A in B *^ C & A in C *^ B ) by A1; :: thesis: verum