set P = closed_inside_of_rectangle (a,b,c,d);
A1:
closed_inside_of_rectangle (a,b,c,d) = { p where p is Point of (TOP-REAL 2) : ( a <= p `1 & p `1 <= b & c <= p `2 & p `2 <= d ) }
by JGRAPH_6:def 2;
let w1, w2 be Point of (TOP-REAL 2); JORDAN1:def 1 ( not w1 in closed_inside_of_rectangle (a,b,c,d) or not w2 in closed_inside_of_rectangle (a,b,c,d) or LSeg (w1,w2) c= closed_inside_of_rectangle (a,b,c,d) )
assume
( w1 in closed_inside_of_rectangle (a,b,c,d) & w2 in closed_inside_of_rectangle (a,b,c,d) )
; LSeg (w1,w2) c= closed_inside_of_rectangle (a,b,c,d)
then A2:
( ex p3 being Point of (TOP-REAL 2) st
( p3 = w1 & a <= p3 `1 & p3 `1 <= b & c <= p3 `2 & p3 `2 <= d ) & ex p4 being Point of (TOP-REAL 2) st
( p4 = w2 & a <= p4 `1 & p4 `1 <= b & c <= p4 `2 & p4 `2 <= d ) )
by A1;
let x be object ; TARSKI:def 3 ( not x in LSeg (w1,w2) or x in closed_inside_of_rectangle (a,b,c,d) )
assume
x in LSeg (w1,w2)
; x in closed_inside_of_rectangle (a,b,c,d)
then consider l being Real such that
A3:
x = ((1 - l) * w1) + (l * w2)
and
A4:
( 0 <= l & l <= 1 )
;
set w = ((1 - l) * w1) + (l * w2);
A5:
((1 - l) * w1) + (l * w2) = |[((((1 - l) * w1) `1) + ((l * w2) `1)),((((1 - l) * w1) `2) + ((l * w2) `2))]|
by EUCLID:55;
A6:
l * w2 = |[(l * (w2 `1)),(l * (w2 `2))]|
by EUCLID:57;
then A7:
(l * w2) `2 = l * (w2 `2)
;
A8:
(1 - l) * w1 = |[((1 - l) * (w1 `1)),((1 - l) * (w1 `2))]|
by EUCLID:57;
then
((1 - l) * w1) `2 = (1 - l) * (w1 `2)
;
then
(((1 - l) * w1) + (l * w2)) `2 = ((1 - l) * (w1 `2)) + (l * (w2 `2))
by A5, A7;
then A9:
( c <= (((1 - l) * w1) + (l * w2)) `2 & (((1 - l) * w1) + (l * w2)) `2 <= d )
by A2, A4, XREAL_1:173, XREAL_1:174;
A10:
(l * w2) `1 = l * (w2 `1)
by A6;
((1 - l) * w1) `1 = (1 - l) * (w1 `1)
by A8;
then
(((1 - l) * w1) + (l * w2)) `1 = ((1 - l) * (w1 `1)) + (l * (w2 `1))
by A5, A10;
then
( a <= (((1 - l) * w1) + (l * w2)) `1 & (((1 - l) * w1) + (l * w2)) `1 <= b )
by A2, A4, XREAL_1:173, XREAL_1:174;
hence
x in closed_inside_of_rectangle (a,b,c,d)
by A1, A3, A9; verum