let x0, y0 be Real; :: thesis: for P being Subset of (TOP-REAL 2) st P = { |[x,y0]| where x is Real : x <= x0 } holds
P is convex
let P be Subset of (TOP-REAL 2); :: thesis: ( P = { |[x,y0]| where x is Real : x <= x0 } implies P is convex )
assume A1: P = { |[x,y0]| where x is Real : x <= x0 } ; :: thesis: P is convex
let w1, w2 be Point of (TOP-REAL 2); :: according to JORDAN1:def 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 x1 being Real such that
A4: w1 = |[x1,y0]| and
A5: x1 <= x0 by A1, A2;
consider x2 being Real such that
A6: w2 = |[x2,y0]| and
A7: x2 <= x0 by A1, A3;
let v be set ; :: according to TARSKI:def 3 :: thesis: ( not v in LSeg w1,w2 or v in P )
assume A8: v in LSeg w1,w2 ; :: thesis: v in P
then reconsider v1 = v as Point of (TOP-REAL 2) ;
v1 in { (((1 - l) * w1) + (l * w2)) where l is Real : ( 0 <= l & l <= 1 ) } by A8;
then consider l being Real such that
A9: v1 = ((1 - l) * w1) + (l * w2) and
A10: 0 <= l and
A11: l <= 1 ;
A12: v1 = |[((1 - l) * x1),((1 - l) * y0)]| + (l * |[x2,y0]|) by A4, A6, A9, EUCLID:62
.= |[((1 - l) * x1),((1 - l) * y0)]| + |[(l * x2),(l * y0)]| by EUCLID:62
.= |[(((1 - l) * x1) + (l * x2)),(((1 - l) * y0) + (l * y0))]| by EUCLID:60
.= |[(((1 - l) * x1) + (l * x2)),(1 * y0)]| ;
((1 - l) * x1) + (l * x2) <= x0 by A5, A7, A10, A11, XREAL_1:176;
hence v in P by A1, A12; :: thesis: verum