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 13, TOPMETR:def 1
.= abs (x - y) by A2, METRIC_1:def 12 ; :: thesis: verum