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:22;
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;
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:22;
assume A7: R = { |.(q1 - p).| where p is Point of (TOP-REAL n) : p in Line (p1,p2) } ; :: thesis:
A8: for s being Real st 0 < s holds
ex r being Real st
( r in R & r < |.(q1 - q2).| + s )

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

end;

let r be Real; :: 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:67;
then reconsider x = p0 as Element of REAL n ;
thus |.(q1 - q2).| <= r by A2, A6, A12; :: thesis:

end;

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

end;