let s1, t1, s2, t2 be Real; for P being Subset of (TOP-REAL 2) st P = { |[s,t]| where s, t is Real : ( s1 < s & s < s2 & t1 < t & t < t2 ) } holds
P is convex
let P be Subset of (TOP-REAL 2); ( P = { |[s,t]| where s, t is Real : ( s1 < s & s < s2 & t1 < t & t < t2 ) } implies P is convex )
assume A1:
P = { |[s,t]| where s, t is Real : ( s1 < s & s < s2 & t1 < t & t < t2 ) }
; 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 set ; 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:
s1 < s3
and
A7:
s3 < s2
and
A8:
t1 < t3
and
A9:
t3 < t2
by A1, A2;
A10:
w1 `1 = s3
by A5, EUCLID:56;
A11:
w1 `2 = t3
by A5, EUCLID:56;
consider s4, t4 being Real such that
A12:
|[s4,t4]| = w2
and
A13:
s1 < s4
and
A14:
s4 < s2
and
A15:
t1 < t4
and
A16:
t4 < t2
by A1, A3;
A17:
w2 `1 = s4
by A12, EUCLID:56;
A18:
w2 `2 = t4
by A12, EUCLID:56;
consider l being Real such that
A19:
x = ((1 - l) * w1) + (l * w2)
and
A20:
0 <= l
and
A21:
l <= 1
by A4;
set w = ((1 - l) * w1) + (l * w2);
A22:
((1 - l) * w1) + (l * w2) = |[((((1 - l) * w1) `1 ) + ((l * w2) `1 )),((((1 - l) * w1) `2 ) + ((l * w2) `2 ))]|
by EUCLID:59;
A23:
(1 - l) * w1 = |[((1 - l) * (w1 `1 )),((1 - l) * (w1 `2 ))]|
by EUCLID:61;
A24:
l * w2 = |[(l * (w2 `1 )),(l * (w2 `2 ))]|
by EUCLID:61;
A25:
((1 - l) * w1) `1 = (1 - l) * (w1 `1 )
by A23, EUCLID:56;
A26:
((1 - l) * w1) `2 = (1 - l) * (w1 `2 )
by A23, EUCLID:56;
A27:
(l * w2) `1 = l * (w2 `1 )
by A24, EUCLID:56;
A28:
(l * w2) `2 = l * (w2 `2 )
by A24, EUCLID:56;
A29:
(((1 - l) * w1) + (l * w2)) `1 = ((1 - l) * (w1 `1 )) + (l * (w2 `1 ))
by A22, A25, A27, EUCLID:56;
A30:
(((1 - l) * w1) + (l * w2)) `2 = ((1 - l) * (w1 `2 )) + (l * (w2 `2 ))
by A22, A26, A28, EUCLID:56;
A31:
s1 < (((1 - l) * w1) + (l * w2)) `1
by A6, A10, A13, A17, A20, A21, A29, XREAL_1:177;
A32:
(((1 - l) * w1) + (l * w2)) `1 < s2
by A7, A10, A14, A17, A20, A21, A29, XREAL_1:178;
A33:
t1 < (((1 - l) * w1) + (l * w2)) `2
by A8, A11, A15, A18, A20, A21, A30, XREAL_1:177;
A34:
(((1 - l) * w1) + (l * w2)) `2 < t2
by A9, A11, A16, A18, A20, A21, A30, XREAL_1:178;
((1 - l) * w1) + (l * w2) = |[((((1 - l) * w1) + (l * w2)) `1 ),((((1 - l) * w1) + (l * w2)) `2 )]|
by EUCLID:57;
hence
x in P
by A1, A19, A31, A32, A33, A34; verum