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