let A, B, C be Ordinal; :: thesis: ( A in B & ( C c= A or C in A ) implies A -^ C in B -^ C )
assume that
A1: A in B and
A2: ( C c= A or C in A ) ; :: thesis: A -^ C in B -^ C
A c= B by A1, ORDINAL1:def 2;
then C c= B by A2, ORDINAL1:def 2;
then A3: B = C +^ (B -^ C) by Def5;
C c= A by A2, ORDINAL1:def 2;
then A = C +^ (A -^ C) by Def5;
hence A -^ C in B -^ C by A1, A3, Th22; :: thesis: verum