let x, y, z be ExtReal; :: thesis: ( y is real implies (z - y) + (y - x) = z - x )
assume A1: y is real ; :: thesis: (z - y) + (y - x) = z - x
thus (z - y) + (y - x) = (z - y) - (x - y) by Th27
.= z - x by A1, Th33 ; :: thesis: verum