let y, z, x be ext-real number ; :: thesis: ( y is real implies (z - y) + (y - x) = z - x )
assume Z: y is real ; :: thesis: (z - y) + (y - x) = z - x
thus (z - y) + (y - x) = (z - y) - (x - y) by Th30
.= z - x by Z, Th22 ; :: thesis: verum