theorem :: ORDINAL3:57

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