let B, C, D be Ordinal; :: thesis: ( B +^ C c= B +^ D implies C c= D )
assume A1: B +^ C c= B +^ D ; :: thesis: C c= D
( ( B +^ C c= B +^ D & B +^ C <> B +^ D ) iff B +^ C c< B +^ D ) ;
then ( C = D or C in D ) by A1, Th21, Th22, ORDINAL1:11;
hence C c= D by ORDINAL1:def 2; :: thesis: verum