theorem Th52: :: ORDINAL3:52

for A, B being Ordinal holds (A +^ B) -^ A = B