let B, C, D be Ordinal; :: thesis: ( B +^ C = B +^ D implies C = D )
assume A1: ( B +^ C = B +^ D & C <> D ) ; :: thesis: contradiction
then ( C in D or D in C ) by ORDINAL1:24;
then B +^ C in B +^ C by A1, ORDINAL2:49;
hence contradiction ; :: thesis: verum