theorem Th23: :: ORDINAL3:23

for B, C, D being Ordinal st B +^ C c= B +^ D holds
C c= D