let n be Nat; for x1, x2, y1, y2 being Element of REAL n st y1 in Line (x1,x2) & y2 in Line (x1,x2) & y1 <> y2 holds
Line (x1,x2) c= Line (y1,y2)
let x1, x2, y1, y2 be Element of REAL n; ( y1 in Line (x1,x2) & y2 in Line (x1,x2) & y1 <> y2 implies Line (x1,x2) c= Line (y1,y2) )
assume
y1 in Line (x1,x2)
; ( not y2 in Line (x1,x2) or not y1 <> y2 or Line (x1,x2) c= Line (y1,y2) )
then consider t being Real such that
A1:
y1 = ((1 - t) * x1) + (t * x2)
;
assume
y2 in Line (x1,x2)
; ( not y1 <> y2 or Line (x1,x2) c= Line (y1,y2) )
then consider s being Real such that
A2:
y2 = ((1 - s) * x1) + (s * x2)
;
assume
y1 <> y2
; Line (x1,x2) c= Line (y1,y2)
then A3:
t - s <> 0
by A1, A2;
then ((1 - ((t - 1) / (t - s))) * y1) + (((t - 1) / (t - s)) * y2) =
((((1 * (t - s)) - (t - 1)) / (t - s)) * y1) + (((t - 1) / (t - s)) * y2)
by XCMPLX_1:127
.=
(((((- s) + 1) / (t - s)) * ((1 - t) * x1)) + ((((- s) + 1) / (t - s)) * (t * x2))) + (((t - 1) / (t - s)) * (((1 - s) * x1) + (s * x2)))
by A1, A2, RVSUM_1:51
.=
(((((- s) + 1) / (t - s)) * ((1 - t) * x1)) + ((((- s) + 1) / (t - s)) * (t * x2))) + ((((t - 1) / (t - s)) * ((1 - s) * x1)) + (((t - 1) / (t - s)) * (s * x2)))
by RVSUM_1:51
.=
((((((- s) + 1) / (t - s)) * (1 - t)) * x1) + ((((- s) + 1) / (t - s)) * (t * x2))) + ((((t - 1) / (t - s)) * ((1 - s) * x1)) + (((t - 1) / (t - s)) * (s * x2)))
by RVSUM_1:49
.=
((((((- s) + 1) / (t - s)) * (1 - t)) * x1) + (((((- s) + 1) / (t - s)) * t) * x2)) + ((((t - 1) / (t - s)) * ((1 - s) * x1)) + (((t - 1) / (t - s)) * (s * x2)))
by RVSUM_1:49
.=
((((((- s) + 1) / (t - s)) * (1 - t)) * x1) + (((((- s) + 1) / (t - s)) * t) * x2)) + (((((t - 1) / (t - s)) * (1 - s)) * x1) + (((t - 1) / (t - s)) * (s * x2)))
by RVSUM_1:49
.=
((((((- s) + 1) / (t - s)) * (1 - t)) * x1) + (((((- s) + 1) / (t - s)) * t) * x2)) + (((((t - 1) / (t - s)) * (1 - s)) * x1) + ((((t - 1) / (t - s)) * s) * x2))
by RVSUM_1:49
.=
((((((- s) + 1) * (1 / (t - s))) * (1 - t)) * x1) + (((((- s) + 1) / (t - s)) * t) * x2)) + (((((t - 1) / (t - s)) * (1 - s)) * x1) + ((((t - 1) / (t - s)) * s) * x2))
by XCMPLX_1:99
.=
((((((- s) + 1) * (1 - t)) * (1 / (t - s))) * x1) + (((((- s) + 1) / (t - s)) * t) * x2)) + (((((t - 1) / (t - s)) * (1 - s)) * x1) + ((((t - 1) / (t - s)) * s) * x2))
.=
((((((- s) + 1) * (1 - t)) / (t - s)) * x1) + (((((- s) + 1) / (t - s)) * t) * x2)) + (((((t - 1) / (t - s)) * (1 - s)) * x1) + ((((t - 1) / (t - s)) * s) * x2))
by XCMPLX_1:99
.=
((((((- s) + 1) * (1 - t)) / (t - s)) * x1) + (((((- s) + 1) * (1 / (t - s))) * t) * x2)) + (((((t - 1) / (t - s)) * (1 - s)) * x1) + ((((t - 1) / (t - s)) * s) * x2))
by XCMPLX_1:99
.=
((((((- s) + 1) * (1 - t)) / (t - s)) * x1) + (((((- s) + 1) * t) * (1 / (t - s))) * x2)) + (((((t - 1) / (t - s)) * (1 - s)) * x1) + ((((t - 1) / (t - s)) * s) * x2))
.=
((((((- s) + 1) * (1 - t)) / (t - s)) * x1) + (((((- s) + 1) * t) / (t - s)) * x2)) + (((((t - 1) / (t - s)) * (1 - s)) * x1) + ((((t - 1) / (t - s)) * s) * x2))
by XCMPLX_1:99
.=
((((((- s) + 1) * (1 - t)) / (t - s)) * x1) + (((((- s) + 1) * t) / (t - s)) * x2)) + (((((t - 1) * (1 / (t - s))) * (1 - s)) * x1) + ((((t - 1) / (t - s)) * s) * x2))
by XCMPLX_1:99
.=
((((((- s) + 1) * (1 - t)) / (t - s)) * x1) + (((((- s) + 1) * t) / (t - s)) * x2)) + (((((t - 1) * (1 - s)) * (1 / (t - s))) * x1) + ((((t - 1) / (t - s)) * s) * x2))
.=
((((((- s) + 1) * (1 - t)) / (t - s)) * x1) + (((((- s) + 1) * t) / (t - s)) * x2)) + (((((t - 1) * (1 - s)) / (t - s)) * x1) + ((((t - 1) / (t - s)) * s) * x2))
by XCMPLX_1:99
.=
((((((- s) + 1) * (1 - t)) / (t - s)) * x1) + (((((- s) + 1) * t) / (t - s)) * x2)) + (((((t - 1) * (1 - s)) / (t - s)) * x1) + ((((t - 1) * (1 / (t - s))) * s) * x2))
by XCMPLX_1:99
.=
((((((- s) + 1) * (1 - t)) / (t - s)) * x1) + (((((- s) + 1) * t) / (t - s)) * x2)) + (((((t - 1) * (1 - s)) / (t - s)) * x1) + ((((t - 1) * s) * (1 / (t - s))) * x2))
.=
((((((- s) + 1) * (1 - t)) / (t - s)) * x1) + (((((- s) + 1) * t) / (t - s)) * x2)) + (((((t - 1) * (1 - s)) / (t - s)) * x1) + ((((t - 1) * s) / (t - s)) * x2))
by XCMPLX_1:99
.=
(((((- s) + 1) * (1 - t)) / (t - s)) * x1) + ((((((- s) + 1) * t) / (t - s)) * x2) + (((((t - 1) * (1 - s)) / (t - s)) * x1) + ((((t - 1) * s) / (t - s)) * x2)))
by FINSEQOP:28
.=
(((((- s) + 1) * (1 - t)) / (t - s)) * x1) + (((((t - 1) * (1 - s)) / (t - s)) * x1) + ((((((- s) + 1) * t) / (t - s)) * x2) + ((((t - 1) * s) / (t - s)) * x2)))
by Lm2
.=
((((((- s) + 1) * (1 - t)) / (t - s)) * x1) + ((((t - 1) * (1 - s)) / (t - s)) * x1)) + ((((((- s) + 1) * t) / (t - s)) * x2) + ((((t - 1) * s) / (t - s)) * x2))
by FINSEQOP:28
.=
((((((- s) + 1) * (1 - t)) / (t - s)) + (((t - 1) * (1 - s)) / (t - s))) * x1) + ((((((- s) + 1) * t) / (t - s)) * x2) + ((((t - 1) * s) / (t - s)) * x2))
by RVSUM_1:50
.=
((((((- s) + 1) * (1 - t)) / (t - s)) + (((t - 1) * (1 - s)) / (t - s))) * x1) + ((((((- s) + 1) * t) / (t - s)) + (((t - 1) * s) / (t - s))) * x2)
by RVSUM_1:50
.=
((((((- s) + 1) * (1 - t)) + ((t - 1) * (1 - s))) / (t - s)) * x1) + ((((((- s) + 1) * t) / (t - s)) + (((t - 1) * s) / (t - s))) * x2)
by XCMPLX_1:62
.=
(((((1 - t) * (1 - s)) + (- ((1 - t) * (1 - s)))) / (t - s)) * x1) + ((((((- s) + 1) * t) + ((t - 1) * s)) / (t - s)) * x2)
by XCMPLX_1:62
.=
(0* n) + ((((((- s) + 1) * t) + ((t - 1) * s)) / (t - s)) * x2)
by Th3
.=
((1 * (t - s)) / (t - s)) * x2
by Th1
.=
1 * x2
by A3, XCMPLX_1:89
.=
x2
by Th3
;
then A4:
x2 in Line (y1,y2)
;
((1 - (t / (t - s))) * y1) + ((t / (t - s)) * y2) =
((((1 * (t - s)) - t) / (t - s)) * y1) + ((t / (t - s)) * y2)
by A3, XCMPLX_1:127
.=
((((- s) / (t - s)) * ((1 - t) * x1)) + (((- s) / (t - s)) * (t * x2))) + ((t / (t - s)) * (((1 - s) * x1) + (s * x2)))
by A1, A2, RVSUM_1:51
.=
((((- s) / (t - s)) * ((1 - t) * x1)) + (((- s) / (t - s)) * (t * x2))) + (((t / (t - s)) * ((1 - s) * x1)) + ((t / (t - s)) * (s * x2)))
by RVSUM_1:51
.=
(((((- s) / (t - s)) * (1 - t)) * x1) + (((- s) / (t - s)) * (t * x2))) + (((t / (t - s)) * ((1 - s) * x1)) + ((t / (t - s)) * (s * x2)))
by RVSUM_1:49
.=
(((((- s) / (t - s)) * (1 - t)) * x1) + ((((- s) / (t - s)) * t) * x2)) + (((t / (t - s)) * ((1 - s) * x1)) + ((t / (t - s)) * (s * x2)))
by RVSUM_1:49
.=
(((((- s) / (t - s)) * (1 - t)) * x1) + ((((- s) / (t - s)) * t) * x2)) + ((((t / (t - s)) * (1 - s)) * x1) + ((t / (t - s)) * (s * x2)))
by RVSUM_1:49
.=
(((((- s) / (t - s)) * (1 - t)) * x1) + ((((- s) / (t - s)) * t) * x2)) + ((((t / (t - s)) * (1 - s)) * x1) + (((t / (t - s)) * s) * x2))
by RVSUM_1:49
.=
(((((- s) * (1 / (t - s))) * (1 - t)) * x1) + ((((- s) / (t - s)) * t) * x2)) + ((((t / (t - s)) * (1 - s)) * x1) + (((t / (t - s)) * s) * x2))
by XCMPLX_1:99
.=
(((((- s) * (1 - t)) * (1 / (t - s))) * x1) + ((((- s) / (t - s)) * t) * x2)) + ((((t / (t - s)) * (1 - s)) * x1) + (((t / (t - s)) * s) * x2))
.=
(((((- s) * (1 - t)) / (t - s)) * x1) + ((((- s) / (t - s)) * t) * x2)) + ((((t / (t - s)) * (1 - s)) * x1) + (((t / (t - s)) * s) * x2))
by XCMPLX_1:99
.=
(((((- s) * (1 - t)) / (t - s)) * x1) + ((((- s) * (1 / (t - s))) * t) * x2)) + ((((t / (t - s)) * (1 - s)) * x1) + (((t / (t - s)) * s) * x2))
by XCMPLX_1:99
.=
(((((- s) * (1 - t)) / (t - s)) * x1) + ((((- s) * t) * (1 / (t - s))) * x2)) + ((((t / (t - s)) * (1 - s)) * x1) + (((t / (t - s)) * s) * x2))
.=
(((((- s) * (1 - t)) / (t - s)) * x1) + ((((- s) * t) / (t - s)) * x2)) + ((((t / (t - s)) * (1 - s)) * x1) + (((t / (t - s)) * s) * x2))
by XCMPLX_1:99
.=
(((((- s) * (1 - t)) / (t - s)) * x1) + ((((- s) * t) / (t - s)) * x2)) + ((((t * (1 / (t - s))) * (1 - s)) * x1) + (((t / (t - s)) * s) * x2))
by XCMPLX_1:99
.=
(((((- s) * (1 - t)) / (t - s)) * x1) + ((((- s) * t) / (t - s)) * x2)) + ((((t * (1 - s)) * (1 / (t - s))) * x1) + (((t / (t - s)) * s) * x2))
.=
(((((- s) * (1 - t)) / (t - s)) * x1) + ((((- s) * t) / (t - s)) * x2)) + ((((t * (1 - s)) / (t - s)) * x1) + (((t / (t - s)) * s) * x2))
by XCMPLX_1:99
.=
(((((- s) * (1 - t)) / (t - s)) * x1) + ((((- s) * t) / (t - s)) * x2)) + ((((t * (1 - s)) / (t - s)) * x1) + (((t * (1 / (t - s))) * s) * x2))
by XCMPLX_1:99
.=
(((((- s) * (1 - t)) / (t - s)) * x1) + ((((- s) * t) / (t - s)) * x2)) + ((((t * (1 - s)) / (t - s)) * x1) + (((t * s) * (1 / (t - s))) * x2))
.=
(((((- s) * (1 - t)) / (t - s)) * x1) + ((((- s) * t) / (t - s)) * x2)) + ((((t * (1 - s)) / (t - s)) * x1) + (((t * s) / (t - s)) * x2))
by XCMPLX_1:99
.=
((((- s) * (1 - t)) / (t - s)) * x1) + (((((- s) * t) / (t - s)) * x2) + ((((t * (1 - s)) / (t - s)) * x1) + (((t * s) / (t - s)) * x2)))
by FINSEQOP:28
.=
((((- s) * (1 - t)) / (t - s)) * x1) + ((((t * (1 - s)) / (t - s)) * x1) + (((((- s) * t) / (t - s)) * x2) + (((t * s) / (t - s)) * x2)))
by Lm2
.=
(((((- s) * (1 - t)) / (t - s)) * x1) + (((t * (1 - s)) / (t - s)) * x1)) + (((((- s) * t) / (t - s)) * x2) + (((t * s) / (t - s)) * x2))
by FINSEQOP:28
.=
(((((- s) * (1 - t)) / (t - s)) + ((t * (1 - s)) / (t - s))) * x1) + (((((- s) * t) / (t - s)) * x2) + (((t * s) / (t - s)) * x2))
by RVSUM_1:50
.=
(((((- s) * (1 - t)) / (t - s)) + ((t * (1 - s)) / (t - s))) * x1) + (((((- s) * t) / (t - s)) + ((t * s) / (t - s))) * x2)
by RVSUM_1:50
.=
(((((- s) * (1 - t)) + (t * (1 - s))) / (t - s)) * x1) + (((((- s) * t) / (t - s)) + ((t * s) / (t - s))) * x2)
by XCMPLX_1:62
.=
(((((- s) * (1 - t)) + (t * (1 - s))) / (t - s)) * x1) + (((((- s) * t) + (t * s)) / (t - s)) * x2)
by XCMPLX_1:62
.=
(((((- s) * (1 - t)) + (t * (1 - s))) / (t - s)) * x1) + (0* n)
by Th3
.=
((1 * (t - s)) / (t - s)) * x1
by Th1
.=
1 * x1
by A3, XCMPLX_1:89
.=
x1
by Th3
;
then
x1 in Line (y1,y2)
;
hence
Line (x1,x2) c= Line (y1,y2)
by A4, Th10; verum