let s1, t be real number ; for P being Subset of (TOP-REAL 2) st P = { |[s,t]| where s is Real : s1 < s } holds
P is convex
let P be Subset of (TOP-REAL 2); ( P = { |[s,t]| where s is Real : s1 < s } implies P is convex )
assume A1:
P = { |[s,t]| where s is Real : s1 < s }
; 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 s3 being Real such that
A4:
|[s3,t]| = w1
and
A5:
s1 < s3
by A1, A2;
consider s4 being Real such that
A6:
|[s4,t]| = w2
and
A7:
s1 < s4
by A1, A3;
A8:
w2 `1 = s4
by A6, EUCLID:56;
let x be set ; 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
A9:
x = ((1 - l) * w1) + (l * w2)
and
A10:
( 0 <= l & l <= 1 )
;
set w = ((1 - l) * w1) + (l * w2);
A11:
((1 - l) * w1) + (l * w2) = |[((((1 - l) * w1) `1 ) + ((l * w2) `1 )),((((1 - l) * w1) `2 ) + ((l * w2) `2 ))]|
by EUCLID:59;
A12:
l * w2 = |[(l * (w2 `1 )),(l * (w2 `2 ))]|
by EUCLID:61;
then A13:
(l * w2) `1 = l * (w2 `1 )
by EUCLID:56;
A14:
(1 - l) * w1 = |[((1 - l) * (w1 `1 )),((1 - l) * (w1 `2 ))]|
by EUCLID:61;
then
((1 - l) * w1) `1 = (1 - l) * (w1 `1 )
by EUCLID:56;
then A15:
(((1 - l) * w1) + (l * w2)) `1 = ((1 - l) * (w1 `1 )) + (l * (w2 `1 ))
by A11, A13, EUCLID:56;
A16:
(l * w2) `2 = l * (w2 `2 )
by A12, EUCLID:56;
((1 - l) * w1) `2 = (1 - l) * (w1 `2 )
by A14, EUCLID:56;
then A17:
(((1 - l) * w1) + (l * w2)) `2 = ((1 - l) * (w1 `2 )) + (l * (w2 `2 ))
by A11, A16, EUCLID:56;
w2 `2 = t
by A6, EUCLID:56;
then A18: (((1 - l) * w1) + (l * w2)) `2 =
((1 - l) * t) + (l * t)
by A4, A17, EUCLID:56
.=
t - 0
;
A19:
((1 - l) * w1) + (l * w2) = |[((((1 - l) * w1) + (l * w2)) `1 ),((((1 - l) * w1) + (l * w2)) `2 )]|
by EUCLID:57;
w1 `1 = s3
by A4, EUCLID:56;
then
s1 < (((1 - l) * w1) + (l * w2)) `1
by A5, A7, A8, A10, A15, XREAL_1:177;
hence
x in P
by A1, A9, A19, A18; verum