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); :: according to JORDAN1:def 1 :: thesis: ( 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 ) ; :: thesis: 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 set ; :: according to TARSKI:def 3 :: thesis: ( not x in LSeg w1,w2 or x in closed_inside_of_rectangle a,b,c,d )
assume x in LSeg w1,w2 ; :: thesis: 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:59;
A6: l * w2 = |[(l * (w2 `1 )),(l * (w2 `2 ))]| by EUCLID:61;
then A7: (l * w2) `2 = l * (w2 `2 ) by EUCLID:56;
A8: (1 - l) * w1 = |[((1 - l) * (w1 `1 )),((1 - l) * (w1 `2 ))]| by EUCLID:61;
then ((1 - l) * w1) `2 = (1 - l) * (w1 `2 ) by EUCLID:56;
then (((1 - l) * w1) + (l * w2)) `2 = ((1 - l) * (w1 `2 )) + (l * (w2 `2 )) by A5, A7, EUCLID:56;
then A9: ( c <= (((1 - l) * w1) + (l * w2)) `2 & (((1 - l) * w1) + (l * w2)) `2 <= d ) by A2, A4, XREAL_1:175, XREAL_1:176;
A10: (l * w2) `1 = l * (w2 `1 ) by A6, EUCLID:56;
((1 - l) * w1) `1 = (1 - l) * (w1 `1 ) by A8, EUCLID:56;
then (((1 - l) * w1) + (l * w2)) `1 = ((1 - l) * (w1 `1 )) + (l * (w2 `1 )) by A5, A10, EUCLID:56;
then ( a <= (((1 - l) * w1) + (l * w2)) `1 & (((1 - l) * w1) + (l * w2)) `1 <= b ) by A2, A4, XREAL_1:175, XREAL_1:176;
hence x in closed_inside_of_rectangle a,b,c,d by A1, A3, A9; :: thesis: verum