let A, B, C be Ordinal; :: thesis: ( A +^ B in C implies B in C -^ A )
A1: (A +^ B) -^ A = B by Th52;
A c= A +^ B by Th24;
hence ( A +^ B in C implies B in C -^ A ) by A1, Th53; :: thesis: verum