let a be Real; :: thesis: for P being Subset of (TOP-REAL 1) st P = { q where q is Point of (TOP-REAL 1) : ex r being Real st
( q = <*r*> & r < - a ) } holds
P is convex
let P be Subset of (TOP-REAL 1); :: thesis: ( P = { q where q is Point of (TOP-REAL 1) : ex r being Real st
( q = <*r*> & r < - a ) } implies P is convex )
assume A1: P = { q where q is Point of (TOP-REAL 1) : ex r being Real st
( q = <*r*> & r < - a ) } ; :: thesis: P is convex
for w1, w2 being Point of (TOP-REAL 1) st w1 in P & w2 in P holds
LSeg w1,w2 c= P

proof

let w1, w2 be Point of (TOP-REAL 1); :: thesis: ( w1 in P & w2 in P implies LSeg w1,w2 c= P )
assume A2: ( w1 in P & w2 in P ) ; :: thesis: LSeg w1,w2 c= P
then consider q1 being Point of (TOP-REAL 1) such that
A3: ( q1 = w1 & ex r being Real st
( q1 = <*r*> & r < - a ) ) by A1;
consider r1 being Real such that
A4: ( q1 = <*r1*> & r1 < - a ) by A3;
consider q2 being Point of (TOP-REAL 1) such that
A5: ( q2 = w2 & ex r being Real st
( q2 = <*r*> & r < - a ) ) by A1, A2;
consider r2 being Real such that
A6: ( q2 = <*r2*> & r2 < - a ) by A5;
thus LSeg w1,w2 c= P :: thesis: verum

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in LSeg w1,w2 or x in P )
assume x in LSeg w1,w2 ; :: thesis: x in P
then x in { (((1 - r) * w1) + (r * w2)) where r is Real : ( 0 <= r & r <= 1 ) } ;
then consider r3 being Real such that
A7: ( x = ((1 - r3) * w1) + (r3 * w2) & 0 <= r3 & r3 <= 1 ) ;
A8: 1 - r3 >= 0 by A7, XREAL_1:50;

per cases ( r3 > 0 or r3 <= 0 ) ;

suppose A9: r3 > 0 ; :: thesis: x in P

A10: (1 - r3) * r1 <= (1 - r3) * (- a) by A4, A8, XREAL_1:66;
A11: r3 * r2 < r3 * (- a) by A6, A9, XREAL_1:70;
((1 - r3) * (- a)) + (r3 * (- a)) = - a ;
then A12: ((1 - r3) * r1) + (r3 * r2) < - a by A10, A11, XREAL_1:10;
<*(((1 - r3) * r1) + (r3 * r2))*> = |[((1 - r3) * r1)]| + |[(r3 * r2)]| by JORDAN2B:27
.= ((1 - r3) * |[r1]|) + |[(r3 * r2)]| by JORDAN2B:26
.= ((1 - r3) * |[r1]|) + (r3 * |[r2]|) by JORDAN2B:26 ;
hence x in P by A1, A3, A4, A5, A6, A7, A12; :: thesis: verum

end;

suppose r3 <= 0 ; :: thesis: x in P

then r3 = 0 by A7;
then x = w1 + (0 * w2) by A7, EUCLID:33
.= w1 + (0. (TOP-REAL 1)) by EUCLID:33
.= w1 by EUCLID:31 ;
hence x in P by A2; :: thesis: verum

end;

end;

end;

end;

hence P is convex by JORDAN1:def 1; :: thesis: verum