let B, C, D be Ordinal; :: thesis: ( B +^ C in B +^ D implies C in D )
assume A1: ( B +^ C in B +^ D & not C in D ) ; :: thesis: contradiction
then D c= C by ORDINAL1:26;
hence contradiction by A1, ORDINAL1:7, ORDINAL2:50; :: thesis: verum