let s, t1 be real number ; :: thesis: for P being Subset of (TOP-REAL 2) st P = { |[s,t]| where t is Real : t1 < t } holds
P is convex
let P be Subset of (TOP-REAL 2); :: thesis: ( P = { |[s,t]| where t is Real : t1 < t } implies P is convex )
assume A1: P = { |[s,t]| where t is Real : t1 < t } ; :: 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 that
A2: w1 in P and
A3: w2 in P ; :: thesis: LSeg w1,w2 c= P
consider t3 being Real such that
A4: |[s,t3]| = w1 and
A5: t1 < t3 by A1, A2;
A6: w1 `1 = s by A4, EUCLID:56;
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 consider l being Real such that
A7: x = ((1 - l) * w1) + (l * w2) and
A8: ( 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;
consider t4 being Real such that
A10: |[s,t4]| = w2 and
A11: t1 < t4 by A1, A3;
A12: w2 `1 = s by A10, EUCLID:56;
A13: l * w2 = |[(l * (w2 `1 )),(l * (w2 `2 ))]| by EUCLID:61;
then A14: (l * w2) `1 = l * (w2 `1 ) by EUCLID:56;
A15: (l * w2) `2 = l * (w2 `2 ) by A13, EUCLID:56;
A16: (1 - l) * w1 = |[((1 - l) * (w1 `1 )),((1 - l) * (w1 `2 ))]| by EUCLID:61;
then ((1 - l) * w1) `2 = (1 - l) * (w1 `2 ) by EUCLID:56;
then A17: (((1 - l) * w1) + (l * w2)) `2 = ((1 - l) * (w1 `2 )) + (l * (w2 `2 )) by A9, A15, EUCLID:56;
A18: w2 `2 = t4 by A10, EUCLID:56;
((1 - l) * w1) `1 = (1 - l) * (w1 `1 ) by A16, EUCLID:56;
then A19: ( ((1 - l) * w1) + (l * w2) = |[((((1 - l) * w1) + (l * w2)) `1 ),((((1 - l) * w1) + (l * w2)) `2 )]| & (((1 - l) * w1) + (l * w2)) `1 = s - 0 ) by A6, A12, A9, A14, EUCLID:56, EUCLID:57;
w1 `2 = t3 by A4, EUCLID:56;
then t1 < (((1 - l) * w1) + (l * w2)) `2 by A5, A11, A18, A8, A17, XREAL_1:177;
hence x in P by A1, A7, A19; :: thesis: verum