let x0, y0 be Real; 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); ( P = { |[x,y0]| where x is Real : x <= x0 } implies P is convex )
assume A1:
P = { |[x,y0]| where x is Real : x <= x0 }
; P is convex
let w1, w2 be Point of (TOP-REAL 2); JORDAN1:def 1 ( w1 in P & w2 in P implies LSeg (w1,w2) c= P )
assume that
A2:
w1 in P
and
A3:
w2 in P
; 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 object ; TARSKI:def 3 ( not v in LSeg (w1,w2) or v in P )
assume A8:
v in LSeg (w1,w2)
; 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) * x1),((1 - l) * y0)]| + (l * |[x2,y0]|)
by A4, A6, A9, EUCLID:58
.=
|[((1 - l) * x1),((1 - l) * y0)]| + |[(l * x2),(l * y0)]|
by EUCLID:58
.=
|[(((1 - l) * x1) + (l * x2)),(((1 - l) * y0) + (l * y0))]|
by EUCLID:56
.=
|[(((1 - l) * x1) + (l * x2)),(1 * y0)]|
;
((1 - l) * x1) + (l * x2) <= x0
by A5, A7, A10, A11, XREAL_1:174;
hence
v in P
by A1, A12; verum