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 y1 being Real such that
A4: w1 = |[x0,y1]| and
A5: y1 <= y0 by A1, A2;
consider y2 being Real such that
A6: w2 = |[x0,y2]| and
A7: y2 <= 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) ;
consider l being Real such that
A9: v1 = ((1 - l) * w1) + (l * w2) and
A10: 0 <= l and
A11: l <= 1 by A8;
A12: v1 = |[((1 - l) * x0),((1 - l) * y1)]| + (l * |[x0,y2]|) by A4, A6, A9, EUCLID:58
.= |[((1 - l) * x0),((1 - l) * y1)]| + |[(l * x0),(l * y2)]| by EUCLID:58
.= |[(((1 - l) * x0) + (l * x0)),(((1 - l) * y1) + (l * y2))]| by EUCLID:56
.= |[(1 * x0),(((1 - l) * y1) + (l * y2))]| ;
((1 - l) * y1) + (l * y2) <= y0 by A5, A7, A10, A11, XREAL_1:174;
hence v in P by A1, A12; :: thesis: verum