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