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) holds
Line (y1,y2) c= Line (x1,x2)
let x1, x2, y1, y2 be Element of REAL n; ( y1 in Line (x1,x2) & y2 in Line (x1,x2) implies Line (y1,y2) c= Line (x1,x2) )
assume
y1 in Line (x1,x2)
; ( not y2 in Line (x1,x2) or Line (y1,y2) c= Line (x1,x2) )
then consider t being Real such that
A1:
y1 = ((1 - t) * x1) + (t * x2)
;
assume
y2 in Line (x1,x2)
; Line (y1,y2) c= Line (x1,x2)
then consider s being Real such that
A2:
y2 = ((1 - s) * x1) + (s * x2)
;
let z be object ; TARSKI:def 3 ( not z in Line (y1,y2) or z in Line (x1,x2) )
assume
z in Line (y1,y2)
; z in Line (x1,x2)
then consider u being Real such that
A3:
z = ((1 - u) * y1) + (u * y2)
;
z =
(((1 - u) * ((1 - t) * x1)) + ((1 - u) * (t * x2))) + (u * (((1 - s) * x1) + (s * x2)))
by A1, A2, A3, RVSUM_1:51
.=
(((1 - u) * ((1 - t) * x1)) + ((1 - u) * (t * x2))) + ((u * ((1 - s) * x1)) + (u * (s * x2)))
by RVSUM_1:51
.=
((((1 - u) * (1 - t)) * x1) + ((1 - u) * (t * x2))) + ((u * ((1 - s) * x1)) + (u * (s * x2)))
by RVSUM_1:49
.=
((((1 - u) * (1 - t)) * x1) + (((1 - u) * t) * x2)) + ((u * ((1 - s) * x1)) + (u * (s * x2)))
by RVSUM_1:49
.=
((((1 - u) * (1 - t)) * x1) + (((1 - u) * t) * x2)) + (((u * (1 - s)) * x1) + (u * (s * x2)))
by RVSUM_1:49
.=
((((1 - u) * (1 - t)) * x1) + (((1 - u) * t) * x2)) + (((u * (1 - s)) * x1) + ((u * s) * x2))
by RVSUM_1:49
.=
(((1 - u) * (1 - t)) * x1) + ((((1 - u) * t) * x2) + (((u * (1 - s)) * x1) + ((u * s) * x2)))
by FINSEQOP:28
.=
(((1 - u) * (1 - t)) * x1) + (((u * (1 - s)) * x1) + ((((1 - u) * t) * x2) + ((u * s) * x2)))
by Lm2
.=
((((1 - u) * (1 - t)) * x1) + ((u * (1 - s)) * x1)) + ((((1 - u) * t) * x2) + ((u * s) * x2))
by FINSEQOP:28
.=
((((1 - u) * (1 - t)) + (u * (1 - s))) * x1) + ((((1 - u) * t) * x2) + ((u * s) * x2))
by RVSUM_1:50
.=
((1 - (((1 * t) - (u * t)) + (u * s))) * x1) + ((((1 * t) - (u * t)) + (u * s)) * x2)
by RVSUM_1:50
;
hence
z in Line (x1,x2)
; verum