let s2 be Real; for P being Subset of (TOP-REAL 2) st P = { |[s,t]| where s, t is Real : s < s2 } holds
P is convex
let P be Subset of (TOP-REAL 2); ( P = { |[s,t]| where s, t is Real : s < s2 } implies P is convex )
assume A1:
P = { |[s,t]| where s, t is Real : s < s2 }
; P is convex
let w1 be Point of (TOP-REAL 2); JORDAN1:def 1 for w2 being Element of (TOP-REAL 2) st w1 in P & w2 in P holds
LSeg (w1,w2) c= P
let w2 be Point of (TOP-REAL 2); ( 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
let x be object ; TARSKI:def 3 ( not x in LSeg (w1,w2) or x in P )
assume A4:
x in LSeg (w1,w2)
; x in P
consider s3, t3 being Real such that
A5:
|[s3,t3]| = w1
and
A6:
s3 < s2
by A1, A2;
A7:
w1 `1 = s3
by A5, EUCLID:52;
consider s4, t4 being Real such that
A8:
|[s4,t4]| = w2
and
A9:
s4 < s2
by A1, A3;
A10:
w2 `1 = s4
by A8, EUCLID:52;
consider l being Real such that
A11:
x = ((1 - l) * w1) + (l * w2)
and
A12:
0 <= l
and
A13:
l <= 1
by A4;
set w = ((1 - l) * w1) + (l * w2);
A14:
((1 - l) * w1) + (l * w2) = |[((((1 - l) * w1) `1) + ((l * w2) `1)),((((1 - l) * w1) `2) + ((l * w2) `2))]|
by EUCLID:55;
A15:
(1 - l) * w1 = |[((1 - l) * (w1 `1)),((1 - l) * (w1 `2))]|
by EUCLID:57;
A16:
l * w2 = |[(l * (w2 `1)),(l * (w2 `2))]|
by EUCLID:57;
A17:
((1 - l) * w1) `1 = (1 - l) * (w1 `1)
by A15, EUCLID:52;
(l * w2) `1 = l * (w2 `1)
by A16, EUCLID:52;
then
(((1 - l) * w1) + (l * w2)) `1 = ((1 - l) * (w1 `1)) + (l * (w2 `1))
by A14, A17, EUCLID:52;
then A18:
s2 > (((1 - l) * w1) + (l * w2)) `1
by A6, A7, A9, A10, A12, A13, XREAL_1:176;
((1 - l) * w1) + (l * w2) = |[((((1 - l) * w1) + (l * w2)) `1),((((1 - l) * w1) + (l * w2)) `2)]|
by EUCLID:53;
hence
x in P
by A1, A11, A18; verum