let A, B, C be Ordinal; :: thesis: ( C <> {} & A in B +^ C implies A -^ B in C )
assume A1: C <> {} ; :: thesis: ( not A in B +^ C or A -^ B in C )
A2: (B +^ C) -^ B = C by Th52;
( not B c= A implies A -^ B = {} ) by Def5;
hence ( not A in B +^ C or A -^ B in C ) by A1, A2, Th8, Th53; :: thesis: verum