let A, B be Ordinal; :: thesis: (A +^ B) -^ A = B
A c= A +^ B by Th24;
hence (A +^ B) -^ A = B by Def5; :: thesis: verum