let A, B, C be Ordinal; :: thesis: ( A in B implies ( A in B +^ C & A in C +^ B ) )
assume A1: A in B ; :: thesis: ( A in B +^ C & A in C +^ B )
A2: B c= C +^ B by Th24;
B c= B +^ C by Th24;
hence ( A in B +^ C & A in C +^ B ) by A1, A2; :: thesis: verum