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