let x, y be ext-real number ; :: thesis: ( - ((- x) + y) = x - y & - ((- x) + y) = x + (- y) )
- ((- x) + y) = (- (- x)) - y by Th26
.= x - y ;
hence ( - ((- x) + y) = x - y & - ((- x) + y) = x + (- y) ) ; :: thesis: verum