let a, b, c be Point of (TOP-REAL 2); :: thesis: ( b in LSeg (a,c) & a `2 <= b `2 & c `2 <= b `2 & not a = b & not b = c implies ( a `2 = b `2 & c `2 = b `2 ) )
assume that
A1: b in LSeg (a,c) and
A2: ( a `2 <= b `2 & c `2 <= b `2 ) ; :: thesis: ( a = b or b = c or ( a `2 = b `2 & c `2 = b `2 ) )
consider r being Real such that
A3: b = ((1 - r) * a) + (r * c) and
0 <= r and
r <= 1 by A1;

per cases ( ( a `2 = b `2 & c `2 < b `2 ) or ( a `2 < b `2 & c `2 = b `2 ) or ( a `2 < b `2 & c `2 < b `2 ) or ( a `2 = b `2 & c `2 = b `2 ) ) by A2, XXREAL_0:1;

suppose that A4: a `2 = b `2 and
A5: c `2 < b `2 ; :: thesis: ( a = b or b = c or ( a `2 = b `2 & c `2 = b `2 ) )

(b `2) + 0 = (((1 - r) * a) `2) + ((r * c) `2) by A3, TOPREAL3:2
.= (((1 - r) * a) `2) + (r * (c `2)) by TOPREAL3:4
.= ((1 - r) * (b `2)) + (r * (c `2)) by A4, TOPREAL3:4
.= (b `2) + ((r * (c `2)) - (r * (b `2))) ;
then A6: 0 = r * ((c `2) - (b `2)) ;
(c `2) - (b `2) < 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 `2 = b `2 & c `2 = b `2 ) ) ; :: thesis: verum

end;

suppose that A7: a `2 < b `2 and
A8: c `2 = b `2 ; :: thesis: ( a = b or b = c or ( a `2 = b `2 & c `2 = b `2 ) )

b `2 = (((1 - r) * a) `2) + ((r * c) `2) by A3, TOPREAL3:2
.= (((1 - r) * a) `2) + (r * (c `2)) by TOPREAL3:4
.= ((1 - r) * (a `2)) + (r * (b `2)) by A8, TOPREAL3:4 ;
then A9: 0 = (1 - r) * ((a `2) - (b `2)) ;
(a `2) - (b `2) < 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 `2 = b `2 & c `2 = b `2 ) ) ; :: thesis: verum

end;

suppose A10: ( a `2 < b `2 & c `2 < b `2 ) ; :: thesis: ( a = b or b = c or ( a `2 = b `2 & c `2 = b `2 ) )

( a `2 <= c `2 or c `2 <= a `2 ) ;
hence ( a = b or b = c or ( a `2 = b `2 & c `2 = b `2 ) ) by A1, A10, TOPREAL1:4; :: thesis: verum

end;

suppose ( a `2 = b `2 & c `2 = b `2 ) ; :: thesis: ( a = b or b = c or ( a `2 = b `2 & c `2 = b `2 ) )

hence ( a = b or b = c or ( a `2 = b `2 & c `2 = b `2 ) ) ; :: thesis: verum

end;

end;