let B, C, D be Ordinal; :: thesis: ( B +^ C = B +^ D implies C = D )
assume that
A1: B +^ C = B +^ D and
A2: C <> D ; :: thesis: contradiction
( C in D or D in C ) by A2, ORDINAL1:14;
then B +^ C in B +^ C by A1, ORDINAL2:32;
hence contradiction ; :: thesis: verum