let n be Nat; :: thesis:
let R be Subset of REAL ; :: thesis:
let p1, p2, q1 be Point of (TOP-REAL n); :: thesis:
reconsider y1 = q1 as Element of REAL n by EUCLID:25;
consider x1, x2 being Element of REAL n such that
A1: ( p1 = x1 & p2 = x2 ) and
A2: Line x1,x2 = Line p1,p2 by Lm8;
A3: x1 - x2 = p1 - p2 by A1, EUCLID:73;
consider y2 being Element of REAL n such that
A4: y2 in Line x1,x2 and
A5: x1 - x2,y1 - y2 are_orthogonal and
A6: for x being Element of REAL n st x in Line x1,x2 holds
|.(y1 - y2).| <= |.(y1 - x).| by Lm7;
reconsider q2 = y2 as Point of (TOP-REAL n) by EUCLID:25;
assume A7: R = { |.(q1 - p).| where p is Point of (TOP-REAL n) : p in Line p1,p2 } ; :: thesis:
A8: for s being real number st 0 < s holds
ex r being real number st
( r in R & r < |.(q1 - q2).| + s )

let s be real number ; :: thesis:
assume A9: 0 < s ; :: thesis:
take r = |.(q1 - q2).|; :: thesis:
thus ( r in R & r < |.(q1 - q2).| + s ) by A7, A2, A4, A9, XREAL_1:31; :: thesis:

end;

p1 in Line p1,p2 by Th47;
then A10: |.(q1 - p1).| in R by A7;
A11: for r being real number st r in R holds
|.(q1 - q2).| <= r

let r be real number ; :: thesis:
assume r in R ; :: thesis:
then consider p0 being Point of (TOP-REAL n) such that
A12: ( r = |.(q1 - p0).| & p0 in Line p1,p2 ) by A7;
the carrier of (Euclid n) = the carrier of (TOP-REAL n) by EUCLID:71;
then reconsider x = p0 as Element of REAL n ;
( y1 - y2 = q1 - q2 & y1 - x = q1 - p0 ) by EUCLID:73;
hence |.(q1 - q2).| <= r by A2, A6, A12; :: thesis:

end;

take |.(q1 - q2).| ; :: according to XXREAL_2:def 9 :: thesis:
let r be ext-real number ; :: according to XXREAL_2:def 2 :: thesis:
assume r in R ; :: thesis:
then consider p0 being Point of (TOP-REAL n) such that
A12: ( r = |.(q1 - p0).| & p0 in Line p1,p2 ) by A7;
the carrier of (Euclid n) = the carrier of (TOP-REAL n) by EUCLID:71;
then reconsider x = p0 as Element of REAL n ;
( y1 - y2 = q1 - q2 & y1 - x = q1 - p0 ) by EUCLID:73;
hence |.(q1 - q2).| <= r by A2, A6, A12; :: thesis:

end;