let s2, t be Real; :: 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 that
A2: w1 in P and
A3: w2 in P ; :: thesis: LSeg (w1,w2) c= P
consider s3 being Real such that
A4: |[s3,t]| = w1 and
A5: s3 < s2 by A1, A2;
consider s4 being Real such that
A6: |[s4,t]| = w2 and
A7: s4 < s2 by A1, A3;
A8: w2 `1 = s4 by A6, EUCLID:52;
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 l being Real such that
A9: x = ((1 - l) * w1) + (l * w2) and
A10: ( 0 <= l & l <= 1 ) ;
set w = ((1 - l) * w1) + (l * w2);
A11: ((1 - l) * w1) + (l * w2) = |[((((1 - l) * w1) `1) + ((l * w2) `1)),((((1 - l) * w1) `2) + ((l * w2) `2))]| by EUCLID:55;
A12: l * w2 = |[(l * (w2 `1)),(l * (w2 `2))]| by EUCLID:57;
then A13: (l * w2) `1 = l * (w2 `1) by EUCLID:52;
A14: (1 - l) * w1 = |[((1 - l) * (w1 `1)),((1 - l) * (w1 `2))]| by EUCLID:57;
then ((1 - l) * w1) `1 = (1 - l) * (w1 `1) by EUCLID:52;
then A15: (((1 - l) * w1) + (l * w2)) `1 = ((1 - l) * (w1 `1)) + (l * (w2 `1)) by A11, A13, EUCLID:52;
A16: (l * w2) `2 = l * (w2 `2) by A12, EUCLID:52;
((1 - l) * w1) `2 = (1 - l) * (w1 `2) by A14, EUCLID:52;
then A17: (((1 - l) * w1) + (l * w2)) `2 = ((1 - l) * (w1 `2)) + (l * (w2 `2)) by A11, A16, EUCLID:52;
w2 `2 = t by A6, EUCLID:52;
then A18: (((1 - l) * w1) + (l * w2)) `2 = ((1 - l) * t) + (l * t) by A4, A17, EUCLID:52
.= t - 0 ;
A19: ((1 - l) * w1) + (l * w2) = |[((((1 - l) * w1) + (l * w2)) `1),((((1 - l) * w1) + (l * w2)) `2)]| by EUCLID:53;
w1 `1 = s3 by A4, EUCLID:52;
then s2 > (((1 - l) * w1) + (l * w2)) `1 by A5, A7, A8, A10, A15, XREAL_1:176;
hence x in P by A1, A9, A19, A18; :: thesis: verum