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 that
A1: ( A c= B or A in B ) and
A2: C in D ; :: thesis: A +^ C in B +^ D
A3: B +^ C in B +^ D by A2, ORDINAL2:32;
A c= B by A1, ORDINAL1:def 2;
hence A +^ C in B +^ D by A3, ORDINAL1:12, ORDINAL2:34; :: thesis: verum