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 )
( B c= B +^ C & B c= C +^ B ) by Th27;
hence ( A in B +^ C & A in C +^ B ) by A1; :: thesis: verum