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

proof

let y be object ; :: 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 and
A4: t <= 1 and
A5: r = (t * (p `2)) + ((1 - t) * (q `2)) by A1, A2, Th51;
set o = (t * p) + ((1 - t) * q);
reconsider x = (t * p) + ((1 - t) * q) as object ;
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, A4;
hence x in LSeg (p,q) ; :: thesis:
thus y = ((t * p) `2) + ((1 - t) * (q `2)) by A5, TOPREAL3:4
.= ((t * p) `2) + (((1 - t) * q) `2) by TOPREAL3:4
.= ((t * p) + ((1 - t) * q)) `2 by TOPREAL3:2
.= proj2 . x by PSCOMP_1:def 6 ; :: thesis:

end;

given x being object such that x in dom proj2 and
A6: x in LSeg (p,q) and
A7: y = proj2 . x ; :: thesis:
reconsider s = x as Point of (TOP-REAL 2) by A6;
x in LSeg (q,p) by A6;
then consider r being Real such that
A8: s = ((1 - r) * q) + (r * p) and
A9: 0 <= r and
A10: r <= 1 ;
y = s `2 by A7, PSCOMP_1:def 6
.= (((1 - r) * q) `2) + ((r * p) `2) by A8, TOPREAL3:2
.= ((1 - r) * (q `2)) + ((r * p) `2) by TOPREAL3:4
.= ((1 - r) * (q `2)) + (r * (p `2)) by TOPREAL3:4 ;
hence y in [.(p `2),(q `2).] by A1, A9, A10, Th51; :: thesis:

end;

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