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