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 that
A2: w1 in P and
A3: w2 in P ; :: thesis: LSeg (w1,w2) c= P
consider q2 being Point of (TOP-REAL 1) such that
A4: q2 = w2 and
A5: ex r being Real st
( q2 = <*r*> & r > a ) by A1, A3;
consider q1 being Point of (TOP-REAL 1) such that
A6: q1 = w1 and
A7: ex r being Real st
( q1 = <*r*> & r > a ) by A1, A2;
consider r2 being Real such that
A8: q2 = <*r2*> and
A9: r2 > a by A5;
consider r1 being Real such that
A10: q1 = <*r1*> and
A11: r1 > a by A7;
thus LSeg (w1,w2) c= P :: thesis: verum

proof

let x be object ; :: 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 consider r3 being Real such that
A12: x = ((1 - r3) * w1) + (r3 * w2) and
A13: 0 <= r3 and
A14: r3 <= 1 ;
A15: 1 - r3 >= 0 by A14, XREAL_1:48;

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

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

A17: ( (1 - r3) * r1 >= (1 - r3) * a & ((1 - r3) * a) + (r3 * a) = a ) by A11, A15, XREAL_1:64;
r3 * r2 > r3 * a by A9, A16, XREAL_1:68;
then A18: ((1 - r3) * r1) + (r3 * r2) > a by A17, XREAL_1:8;
<*(((1 - r3) * r1) + (r3 * r2))*> = |[((1 - r3) * r1)]| + |[(r3 * r2)]| by JORDAN2B:22
.= ((1 - r3) * |[r1]|) + |[(r3 * r2)]| by JORDAN2B:21
.= ((1 - r3) * |[r1]|) + (r3 * |[r2]|) by JORDAN2B:21 ;
hence x in P by A1, A6, A10, A4, A8, A12, A18; :: thesis: verum

end;

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

then r3 = 0 by A13;
then x = w1 + (0 * w2) by A12, RLVECT_1:def 8
.= w1 + (0. (TOP-REAL 1)) by RLVECT_1:10
.= w1 by RLVECT_1:4 ;
hence x in P by A2; :: thesis: verum

end;

end;

end;

end;

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