let s2, t be real number ; :: thesis: for P being Subset of (TOP-REAL 2) st P = { |[s,t]| where s is Real : s < s2 } holds
P is convex
let P be Subset of (TOP-REAL 2); :: thesis: ( P = { |[s,t]| where s is Real : s < s2 } implies P is convex )
assume A1: P = { |[s,t]| where s is Real : s < s2 } ; :: thesis: P is convex
let w1, w2 be Point of (TOP-REAL 2); :: according to JORDAN1:def 1 :: thesis: ( not w1 in P or not w2 in P or LSeg w1,w2 c= P )
assume A2: ( w1 in P & w2 in P ) ; :: thesis: LSeg w1,w2 c= P
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in LSeg w1,w2 or x in P )
assume A3: x in LSeg w1,w2 ; :: thesis: x in P
consider s3 being Real such that
A4: ( |[s3,t]| = w1 & s3 < s2 ) by A1, A2;
A5: ( w1 `1 = s3 & w1 `2 = t ) by A4, EUCLID:56;
consider s4 being Real such that
A6: ( |[s4,t]| = w2 & s4 < s2 ) by A1, A2;
A7: ( w2 `1 = s4 & w2 `2 = t ) by A6, EUCLID:56;
x in { (((1 - lambda) * w1) + (lambda * w2)) where lambda is Real : ( 0 <= lambda & lambda <= 1 ) } by A3;
then consider l being Real such that
A8: ( x = ((1 - l) * w1) + (l * w2) & 0 <= l & l <= 1 ) ;
set w = ((1 - l) * w1) + (l * w2);
A9: ((1 - l) * w1) + (l * w2) = |[((((1 - l) * w1) `1 ) + ((l * w2) `1 )),((((1 - l) * w1) `2 ) + ((l * w2) `2 ))]| by EUCLID:59;
( (1 - l) * w1 = |[((1 - l) * (w1 `1 )),((1 - l) * (w1 `2 ))]| & l * w2 = |[(l * (w2 `1 )),(l * (w2 `2 ))]| ) by EUCLID:61;
then ( ((1 - l) * w1) `1 = (1 - l) * (w1 `1 ) & ((1 - l) * w1) `2 = (1 - l) * (w1 `2 ) & (l * w2) `1 = l * (w2 `1 ) & (l * w2) `2 = l * (w2 `2 ) ) by EUCLID:56;
then A10: ( (((1 - l) * w1) + (l * w2)) `1 = ((1 - l) * (w1 `1 )) + (l * (w2 `1 )) & (((1 - l) * w1) + (l * w2)) `2 = ((1 - l) * (w1 `2 )) + (l * (w2 `2 )) ) by A9, EUCLID:56;
then A11: ( s2 > (((1 - l) * w1) + (l * w2)) `1 & ((1 - l) * w1) + (l * w2) = |[((((1 - l) * w1) + (l * w2)) `1 ),((((1 - l) * w1) + (l * w2)) `2 )]| ) by A4, A5, A6, A7, A8, EUCLID:57, XREAL_1:178;
(((1 - l) * w1) + (l * w2)) `2 = ((1 - l) * t) + (l * t) by A4, A7, A10, EUCLID:56
.= t - 0 ;
hence x in P by A1, A8, A11; :: thesis: verum