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