let x, y be real number ; :: thesis: for A being SubSpace of RealSpace
for p, q being Point of A st x = p & y = q holds
dist p,q = abs (x - y)
let A be SubSpace of RealSpace ; :: thesis: for p, q being Point of A st x = p & y = q holds
dist p,q = abs (x - y)
let p, q be Point of A; :: 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 = the distance of A . p,q by METRIC_1:def 1
.= real_dist . x,y by A1, METRIC_1:def 14, TOPMETR:def 1
.= abs (x - y) by A2, METRIC_1:def 13 ; :: thesis: verum