let A, B, C be Ordinal; :: thesis: ( A in B & ( C c= A or C in A ) implies A -^ C in B -^ C )
assume A1: ( A in B & ( C c= A or C in A ) ) ; :: thesis: A -^ C in B -^ C
then ( A c= B & C c= A ) by ORDINAL1:def 2;
then A2: ( A = C +^ (A -^ C) & C c= B ) by Def6, XBOOLE_1:1;
then B = C +^ (B -^ C) by Def6;
hence A -^ C in B -^ C by A1, A2, Th25; :: thesis: verum