( not b c= a or b c= a ) ;
then ( a -^ b = {} or a = b +^ (a -^ b) ) by Def6;
hence a -^ b in omega by Th87, ORDINAL1:def 11; :: according to ORDINAL1:def 12 :: thesis: verum