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 & 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:7
.= (((1 - r) * a) `2 ) + (r * (c `2 )) by TOPREAL3:9
.= ((1 - r) * (b `2 )) + (r * (c `2 )) by A4, TOPREAL3:9
.= (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:51;
then r = 0 by A6, XCMPLX_1:6;
then b = (1 * a) + (0. (TOP-REAL 2)) by A3, EUCLID:33
.= 1 * a by EUCLID:31
.= a by EUCLID:33 ;
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:7
.= (((1 - r) * a) `2 ) + (r * (c `2 )) by TOPREAL3:9
.= ((1 - r) * (a `2 )) + (r * (b `2 )) by A8, TOPREAL3:9 ;
then A9: 0 = (1 - r) * ((a `2 ) - (b `2 )) ;
(a `2 ) - (b `2 ) < 0 by A7, XREAL_1:51;
then 1 - r = 0 by A9, XCMPLX_1:6;
then b = (0. (TOP-REAL 2)) + (1 * c) by A3, EUCLID:33
.= 1 * c by EUCLID:31
.= c by EUCLID:33 ;
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:10; :: 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;