let p, q be Point of RealSpace ; :: thesis: for x, y being real number st x = p & y = q holds
dist p,q = abs (x - y)
let x, y be real number ; :: thesis: ( x = p & y = q implies dist p,q = abs (x - y) )
assume A1: ( x = p & y = q ) ; :: thesis: dist p,q = abs (x - y)
A2: ( x is Real & y is Real ) by XREAL_0:def 1;
thus dist p,q = real_dist . x,y by A1, METRIC_1:def 1, METRIC_1:def 14
.= abs (x - y) by A2, METRIC_1:def 13 ; :: thesis: verum