let B, C, D be Ordinal; :: thesis: ( B +^ C in B +^ D implies C in D )
assume that
A1: B +^ C in B +^ D and
A2: not C in D ; :: thesis: contradiction
D c= C by A2, ORDINAL1:16;
hence contradiction by A1, ORDINAL1:5, ORDINAL2:33; :: thesis: verum