let A, B, C be Ordinal; :: thesis: ( A +^ B in C implies B in C -^ A )
A1: (A +^ B) -^ A = B by Th65;
A c= A +^ B by Th27;
hence ( A +^ B in C implies B in C -^ A ) by A1, Th66; :: thesis: verum