theorem :: ORDINAL3:51

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