let x, y be ExtReal; :: thesis: ( - ((- x) + y) = x - y & - ((- x) + y) = x + (- y) )
- ((- x) + y) = (- (- x)) - y by Th25
.= x - y ;
hence ( - ((- x) + y) = x - y & - ((- x) + y) = x + (- y) ) ; :: thesis: verum