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