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

proof

let y be object ; :: thesis:

hereby :: thesis:

assume A2: y in [.(p `1),(q `1).] ; :: 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 `1)) + ((1 - t) * (q `1)) 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 proj1 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) `1) + ((1 - t) * (q `1)) by A5, TOPREAL3:4
.= ((t * p) `1) + (((1 - t) * q) `1) by TOPREAL3:4
.= ((t * p) + ((1 - t) * q)) `1 by TOPREAL3:2
.= proj1 . x by PSCOMP_1:def 5 ; :: thesis:

end;

given x being object such that x in dom proj1 and
A6: x in LSeg (p,q) and
A7: y = proj1 . 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 `1 by A7, PSCOMP_1:def 5
.= (((1 - r) * q) `1) + ((r * p) `1) by A8, TOPREAL3:2
.= ((1 - r) * (q `1)) + ((r * p) `1) by TOPREAL3:4
.= ((1 - r) * (q `1)) + (r * (p `1)) by TOPREAL3:4 ;
hence y in [.(p `1),(q `1).] by A1, A9, A10, Th51; :: thesis:

end;

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