theorem :: ORDINAL3:61

for A, B, C being Ordinal st A +^ B in C holds
B in C -^ A