let x, y be Point of (Euclid 1); for r, s being Real st x = <*r*> & y = <*s*> holds
dist (x,y) = |.(r - s).|
let r, s be Real; ( x = <*r*> & y = <*s*> implies dist (x,y) = |.(r - s).| )
assume that
A1:
x = <*r*>
and
A2:
y = <*s*>
; dist (x,y) = |.(r - s).|
consider x1, y1 being Point of RealSpace, xr, yr being Real such that
x1 = xr
and
y1 = yr
and
A3:
x = <*xr*>
and
A4:
y = <*yr*>
and
dist (x1,y1) = real_dist . (xr,yr)
and
A5:
dist (x1,y1) = (Pitag_dist 1) . (<*xr*>,<*yr*>)
and
A6:
dist (x1,y1) = |.(xr - yr).|
by Th7;
( xr = r & yr = s )
by A3, A1, A2, A4, FINSEQ_1:76;
hence
dist (x,y) = |.(r - s).|
by A5, A6, A3, A4; verum