let a, b, c be Point of (TOP-REAL 2); :: thesis: ( b in LSeg (a,c) & a `1 <= b `1 & c `1 <= b `1 & not a = b & not b = c implies ( a `1 = b `1 & c `1 = b `1 ) )
assume that
A1: b in LSeg (a,c) and
A2: ( a `1 <= b `1 & c `1 <= b `1 ) ; :: thesis: ( a = b or b = c or ( a `1 = b `1 & c `1 = b `1 ) )
consider r being Real such that
A3: b = ((1 - r) * a) + (r * c) and
0 <= r and
r <= 1 by A1;
per cases ( ( a `1 = b `1 & c `1 < b `1 ) or ( a `1 < b `1 & c `1 = b `1 ) or ( a `1 < b `1 & c `1 < b `1 ) or ( a `1 = b `1 & c `1 = b `1 ) ) by A2, XXREAL_0:1;
suppose that A4: a `1 = b `1 and
A5: c `1 < b `1 ; :: thesis: ( a = b or b = c or ( a `1 = b `1 & c `1 = b `1 ) )
(b `1) + 0 = (((1 - r) * a) `1) + ((r * c) `1) by A3, TOPREAL3:2
.= (((1 - r) * a) `1) + (r * (c `1)) by TOPREAL3:4
.= ((1 - r) * (b `1)) + (r * (c `1)) by A4, TOPREAL3:4
.= (b `1) + ((r * (c `1)) - (r * (b `1))) ;
then A6: 0 = r * ((c `1) - (b `1)) ;
(c `1) - (b `1) < 0 by A5, XREAL_1:49;
then r = 0 by A6, XCMPLX_1:6;
then b = (1 * a) + (0. (TOP-REAL 2)) by A3, RLVECT_1:10
.= 1 * a by RLVECT_1:4
.= a by RLVECT_1:def 8 ;
hence ( a = b or b = c or ( a `1 = b `1 & c `1 = b `1 ) ) ; :: thesis: verum
end;
suppose that A7: a `1 < b `1 and
A8: c `1 = b `1 ; :: thesis: ( a = b or b = c or ( a `1 = b `1 & c `1 = b `1 ) )
b `1 = (((1 - r) * a) `1) + ((r * c) `1) by A3, TOPREAL3:2
.= (((1 - r) * a) `1) + (r * (c `1)) by TOPREAL3:4
.= ((1 - r) * (a `1)) + (r * (b `1)) by A8, TOPREAL3:4 ;
then A9: 0 = (1 - r) * ((a `1) - (b `1)) ;
(a `1) - (b `1) < 0 by A7, XREAL_1:49;
then 1 - r = 0 by A9, XCMPLX_1:6;
then b = (0. (TOP-REAL 2)) + (1 * c) by A3, RLVECT_1:10
.= 1 * c by RLVECT_1:4
.= c by RLVECT_1:def 8 ;
hence ( a = b or b = c or ( a `1 = b `1 & c `1 = b `1 ) ) ; :: thesis: verum
end;
suppose A10: ( a `1 < b `1 & c `1 < b `1 ) ; :: thesis: ( a = b or b = c or ( a `1 = b `1 & c `1 = b `1 ) )
( a `1 <= c `1 or c `1 <= a `1 ) ;
hence ( a = b or b = c or ( a `1 = b `1 & c `1 = b `1 ) ) by A1, A10, TOPREAL1:3; :: thesis: verum
end;
suppose ( a `1 = b `1 & c `1 = b `1 ) ; :: thesis: ( a = b or b = c or ( a `1 = b `1 & c `1 = b `1 ) )
hence ( a = b or b = c or ( a `1 = b `1 & c `1 = b `1 ) ) ; :: thesis: verum
end;
end;