let p, q be Point of (TOP-REAL 2); :: thesis:
assume A1: p `2 <= q `2 ; :: thesis:
for y being set holds
( y in [.(p `2 ),(q `2 ).] iff ex x being set st
( x in dom proj2 & x in LSeg p,q & y = proj2 . x ) )

proof

let y be set ; :: thesis:

hereby :: thesis:

assume A2: y in [.(p `2 ),(q `2 ).] ; :: thesis:
then reconsider r = y as Real ;
consider t being Real such that
A3: ( 0 <= t & t <= 1 ) and
A4: r = (t * (p `2 )) + ((1 - t) * (q `2 )) by A1, A2, Th59;
set o = (t * p) + ((1 - t) * q);
reconsider x = (t * p) + ((1 - t) * q) as set ;
take x = x; :: thesis:
(t * p) + ((1 - t) * q) in the carrier of (TOP-REAL 2) ;
hence x in dom proj2 by FUNCT_2:def 1; :: thesis:
(t * p) + ((1 - t) * q) in LSeg q,p by A3;
hence x in LSeg p,q ; :: thesis:
thus y = ((t * p) `2 ) + ((1 - t) * (q `2 )) by A4, TOPREAL3:9
.= ((t * p) `2 ) + (((1 - t) * q) `2 ) by TOPREAL3:9
.= ((t * p) + ((1 - t) * q)) `2 by TOPREAL3:7
.= proj2 . x by PSCOMP_1:def 29 ; :: thesis:

end;

given x being set such that x in dom proj2 and
A5: x in LSeg p,q and
A6: y = proj2 . x ; :: thesis:
reconsider s = x as Point of (TOP-REAL 2) by A5;
x in LSeg q,p by A5;
then consider r being Real such that
A8: s = ((1 - r) * q) + (r * p) and
A7: ( 0 <= r & r <= 1 ) by A5;
y = s `2 by A6, PSCOMP_1:def 29
.= (((1 - r) * q) `2 ) + ((r * p) `2 ) by A8, TOPREAL3:7
.= ((1 - r) * (q `2 )) + ((r * p) `2 ) by TOPREAL3:9
.= ((1 - r) * (q `2 )) + (r * (p `2 )) by TOPREAL3:9 ;
hence y in [.(p `2 ),(q `2 ).] by A1, A7, Th59; :: thesis:

end;

hence proj2 .: (LSeg p,q) = [.(p `2 ),(q `2 ).] by FUNCT_1:def 12; :: thesis: