let A, B, C be Ordinal; ( A in B & C <> {} implies ( A in B *^ C & A in C *^ B ) )
assume that
A1:
A in B
and
A2:
C <> {}
; ( A in B *^ C & A in C *^ B )
{} c= C
;
then
{} c< C
by A2;
then
{} in C
by ORDINAL1:11;
then A3:
1 c= C
by Lm1, ORDINAL1:21;
then A4:
1 *^ B c= C *^ B
by ORDINAL2:41;
A5:
1 *^ B = B
by ORDINAL2:39;
A6:
B *^ 1 = B
by ORDINAL2:39;
B *^ 1 c= B *^ C
by A3, ORDINAL2:42;
hence
( A in B *^ C & A in C *^ B )
by A1, A4, A6, A5; verum