theorem Th30: :: ORDINAL3:30

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