let p, q be Point of (TOP-REAL 2); ( p `1 <= q `1 implies proj1 .: (LSeg p,q) = [.(p `1 ),(q `1 ).] )
assume A1:
p `1 <= q `1
; proj1 .: (LSeg p,q) = [.(p `1 ),(q `1 ).]
for y being set holds
( y in [.(p `1 ),(q `1 ).] iff ex x being set st
( x in dom proj1 & x in LSeg p,q & y = proj1 . x ) )
proof
let y be
set ;
( y in [.(p `1 ),(q `1 ).] iff ex x being set st
( x in dom proj1 & x in LSeg p,q & y = proj1 . x ) )
hereby ( ex x being set st
( x in dom proj1 & x in LSeg p,q & y = proj1 . x ) implies y in [.(p `1 ),(q `1 ).] )
assume A2:
y in [.(p `1 ),(q `1 ).]
;
ex x being set st
( x in dom proj1 & x in LSeg p,q & y = proj1 . x )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, Th59;
set o =
(t * p) + ((1 - t) * q);
reconsider x =
(t * p) + ((1 - t) * q) as
set ;
take x =
x;
( x in dom proj1 & x in LSeg p,q & y = proj1 . x )
(t * p) + ((1 - t) * q) in the
carrier of
(TOP-REAL 2)
;
hence
x in dom proj1
by FUNCT_2:def 1;
( x in LSeg p,q & y = proj1 . x )
(t * p) + ((1 - t) * q) in LSeg q,
p
by A3, A4;
hence
x in LSeg p,
q
;
y = proj1 . xthus y =
((t * p) `1 ) + ((1 - t) * (q `1 ))
by A5, TOPREAL3:9
.=
((t * p) `1 ) + (((1 - t) * q) `1 )
by TOPREAL3:9
.=
((t * p) + ((1 - t) * q)) `1
by TOPREAL3:7
.=
proj1 . x
by PSCOMP_1:def 28
;
verum
end;
given x being
set such that
x in dom proj1
and A6:
x in LSeg p,
q
and A7:
y = proj1 . x
;
y in [.(p `1 ),(q `1 ).]
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 28
.=
(((1 - r) * q) `1 ) + ((r * p) `1 )
by A8, TOPREAL3:7
.=
((1 - r) * (q `1 )) + ((r * p) `1 )
by TOPREAL3:9
.=
((1 - r) * (q `1 )) + (r * (p `1 ))
by TOPREAL3:9
;
hence
y in [.(p `1 ),(q `1 ).]
by A1, A9, A10, Th59;
verum
end;
hence
proj1 .: (LSeg p,q) = [.(p `1 ),(q `1 ).]
by FUNCT_1:def 12; verum