let C, A, B 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 Th65;
( not B c= A implies A -^ B = {} ) by Def6;
hence ( not A in B +^ C or A -^ B in C ) by A1, A2, Th10, Th66; :: thesis: verum