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) )
A1: ( x is Real & y is Real ) by XREAL_0:def 1;
assume ( x = p & y = q ) ; :: thesis: dist p,q = abs (x - y)
hence dist p,q = real_dist . x,y by METRIC_1:def 1, METRIC_1:def 14
.= abs (x - y) by A1, METRIC_1:def 13 ;
:: thesis: verum