let A, B, C, D be Ordinal; :: thesis: ( ( A c= B or A in B ) & C in D implies A +^ C in B +^ D )
assume A1: ( ( A c= B or A in B ) & C in D ) ; :: thesis: A +^ C in B +^ D
then A c= B by ORDINAL1:def 2;
then ( A +^ C c= B +^ C & B +^ C in B +^ D ) by A1, ORDINAL2:49, ORDINAL2:51;
hence A +^ C in B +^ D by ORDINAL1:22; :: thesis: verum