let x0, y0 be Real; :: thesis: for P being Subset of (TOP-REAL 2) st P = { |[x0,y]| where y is Real : y >= y0 } holds
P is convex
let P be Subset of (TOP-REAL 2); :: thesis: ( P = { |[x0,y]| where y is Real : y >= y0 } implies P is convex )
assume A1: P = { |[x0,y]| where y is Real : y >= y0 } ; :: 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 = |[x0,x1]| and
A5: x1 >= y0 by A1, A2;
consider x2 being Real such that
A6: w2 = |[x0,x2]| and
A7: x2 >= y0 by A1, A3;
let v be object ; :: 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) * w2) + (l * w1)) where l is Real : ( 0 <= l & l <= 1 ) } by A8, RLTOPSP1:def 2;
then consider l being Real such that
A9: v1 = ((1 - l) * w2) + (l * w1) and
A10: 0 <= l and
A11: l <= 1 ;
A12: v1 = |[((1 - l) * x0),((1 - l) * x2)]| + (l * |[x0,x1]|) by A4, A6, A9, EUCLID:58
.= |[((1 - l) * x0),((1 - l) * x2)]| + |[(l * x0),(l * x1)]| by EUCLID:58
.= |[(((1 - l) * x0) + (l * x0)),(((1 - l) * x2) + (l * x1))]| by EUCLID:56
.= |[(1 * x0),(((1 - l) * x2) + (l * x1))]| ;
((1 - l) * x2) + (l * x1) >= y0 by A5, A7, A10, A11, XREAL_1:173;
hence v in P by A1, A12; :: thesis: verum