let a, b be Real; :: thesis: for xa, xb being Point of (Euclid 1) st xa = <*a*> & xb = <*b*> holds
dist (xa,xb) = |.(a - b).|
let xa, xb be Point of (Euclid 1); :: thesis: ( xa = <*a*> & xb = <*b*> implies dist (xa,xb) = |.(a - b).| )
assume that
A1: xa = <*a*> and
A2: xb = <*b*> ; :: thesis: dist (xa,xb) = |.(a - b).|
( xa in Euclid 1 & xb in Euclid 1 ) ;
then ( xa in TOP-REAL 1 & xb in TOP-REAL 1 ) by EUCLID:67;
then reconsider ra = xa, rb = xb as Element of REAL 1 by EUCLID:22;
A3: Euclid 1 = MetrStruct(# (REAL 1),(Pitag_dist 1) #) by EUCLID:def 7;
A4: ra = 1 |-> a by A1, FINSEQ_2:59;
rb = 1 |-> b by A2, FINSEQ_2:59;
then |.(ra - rb).| = (sqrt 1) * |.(a - b).| by A4, TOPREALC:11
.= |.(a - b).| by SQUARE_1:18 ;
hence dist (xa,xb) = |.(a - b).| by A3, EUCLID:def 6; :: thesis: verum