let n be Nat; for p1, p2, q1, q2 being Point of (TOP-REAL n) st LSeg (q1,q2) c= LSeg (p1,p2) & p1 in LSeg (q1,q2) & not p1 = q1 holds
p1 = q2
let p1, p2, q1, q2 be Point of (TOP-REAL n); ( LSeg (q1,q2) c= LSeg (p1,p2) & p1 in LSeg (q1,q2) & not p1 = q1 implies p1 = q2 )
assume A1:
LSeg (q1,q2) c= LSeg (p1,p2)
; ( not p1 in LSeg (q1,q2) or p1 = q1 or p1 = q2 )
q2 in LSeg (q1,q2)
by RLTOPSP1:68;
then
q2 in LSeg (p1,p2)
by A1;
then consider s2 being Real such that
A2:
q2 = ((1 - s2) * p1) + (s2 * p2)
and
A3:
0 <= s2
and
s2 <= 1
;
assume
p1 in LSeg (q1,q2)
; ( p1 = q1 or p1 = q2 )
then consider r1 being Real such that
A4:
p1 = ((1 - r1) * q1) + (r1 * q2)
and
A5:
( 0 <= r1 & r1 <= 1 )
;
A6:
q1 in LSeg (q1,q2)
by RLTOPSP1:68;
then
q1 in LSeg (p1,p2)
by A1;
then consider s1 being Real such that
A7:
q1 = ((1 - s1) * p1) + (s1 * p2)
and
A8:
0 <= s1
and
s1 <= 1
;
p1 =
((1 - r1) * (((1 - s1) * p1) + (s1 * p2))) + ((r1 * ((1 - s2) * p1)) + (r1 * (s2 * p2)))
by A4, A7, A2, RLVECT_1:def 5
.=
(((1 - r1) * ((1 - s1) * p1)) + ((1 - r1) * (s1 * p2))) + ((r1 * ((1 - s2) * p1)) + (r1 * (s2 * p2)))
by RLVECT_1:def 5
.=
((((1 - r1) * ((1 - s1) * p1)) + ((1 - r1) * (s1 * p2))) + (r1 * ((1 - s2) * p1))) + (r1 * (s2 * p2))
by RLVECT_1:def 3
.=
(((((1 - r1) * (1 - s1)) * p1) + ((1 - r1) * (s1 * p2))) + (r1 * ((1 - s2) * p1))) + (r1 * (s2 * p2))
by RLVECT_1:def 7
.=
(((((1 - r1) * (1 - s1)) * p1) + (((1 - r1) * s1) * p2)) + (r1 * ((1 - s2) * p1))) + (r1 * (s2 * p2))
by RLVECT_1:def 7
.=
(((((1 - r1) * (1 - s1)) * p1) + (((1 - r1) * s1) * p2)) + ((r1 * (1 - s2)) * p1)) + (r1 * (s2 * p2))
by RLVECT_1:def 7
.=
(((((1 - r1) * (1 - s1)) * p1) + (((1 - r1) * s1) * p2)) + ((r1 * (1 - s2)) * p1)) + ((r1 * s2) * p2)
by RLVECT_1:def 7
.=
(((r1 * s2) * p2) + ((((1 - r1) * s1) * p2) + (((1 - r1) * (1 - s1)) * p1))) + ((r1 * (1 - s2)) * p1)
by RLVECT_1:def 3
.=
((((r1 * s2) * p2) + (((1 - r1) * s1) * p2)) + (((1 - r1) * (1 - s1)) * p1)) + ((r1 * (1 - s2)) * p1)
by RLVECT_1:def 3
.=
((((r1 * s2) + ((1 - r1) * s1)) * p2) + (((1 - r1) * (1 - s1)) * p1)) + ((r1 * (1 - s2)) * p1)
by RLVECT_1:def 6
.=
(((r1 * s2) + ((1 - r1) * s1)) * p2) + ((((1 - r1) * (1 - s1)) * p1) + ((r1 * (1 - s2)) * p1))
by RLVECT_1:def 3
.=
(((r1 * s2) + ((1 - r1) * s1)) * p2) + ((((1 - r1) * (1 - s1)) + (r1 * (1 - s2))) * p1)
by RLVECT_1:def 6
;
then 0. (TOP-REAL n) =
((((r1 * s2) + ((1 - r1) * s1)) * p2) + ((((1 - r1) * (1 - s1)) + (r1 * (1 - s2))) * p1)) - p1
by RLVECT_1:5
.=
(((r1 * s2) + ((1 - r1) * s1)) * p2) + (((((1 - r1) * (1 - s1)) + (r1 * (1 - s2))) * p1) - p1)
by RLVECT_1:def 3
.=
(((r1 * s2) + ((1 - r1) * s1)) * p2) + (((((1 - r1) * (1 - s1)) + (r1 * (1 - s2))) * p1) - (1 * p1))
by RLVECT_1:def 8
.=
(((((1 - r1) * (1 - s1)) + (r1 * (1 - s2))) - 1) * p1) + (((r1 * s2) + ((1 - r1) * s1)) * p2)
by RLVECT_1:35
.=
(((((1 - r1) * (1 - s1)) + (r1 * (1 - s2))) - 1) * p1) - (- (((r1 * s2) + ((1 - r1) * s1)) * p2))
;
then
((((1 - r1) * (1 - s1)) + (r1 * (1 - s2))) - 1) * p1 = - (((r1 * s2) + ((1 - r1) * s1)) * p2)
by RLVECT_1:21;
then
((((1 - r1) * (1 - s1)) + (r1 * (1 - s2))) - 1) * p1 = (- ((r1 * s2) + ((1 - r1) * s1))) * p2
by RLVECT_1:79;
then A9:
( - ((r1 * s2) + ((1 - r1) * s1)) = - 0 or p1 = p2 )
by RLVECT_1:36;
per cases
( (r1 * s2) + ((1 - r1) * s1) = 0 or p1 = p2 )
by A9;
suppose A10:
(r1 * s2) + ((1 - r1) * s1) = 0
;
( p1 = q1 or p1 = q2 )now ( p1 = q1 or p1 = q2 )end; hence
(
p1 = q1 or
p1 = q2 )
;
verum end; end;