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 object ; :: 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:55;
A6: l * w2 = |[(l * (w2 `1)),(l * (w2 `2))]| by EUCLID:57;
then A7: (l * w2) `2 = l * (w2 `2) by EUCLID:52;
A8: (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 (((1 - l) * w1) + (l * w2)) `2 = ((1 - l) * (w1 `2)) + (l * (w2 `2)) by A5, A7, EUCLID:52;
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, EUCLID:52;
((1 - l) * w1) `1 = (1 - l) * (w1 `1) by A8, EUCLID:52;
then (((1 - l) * w1) + (l * w2)) `1 = ((1 - l) * (w1 `1)) + (l * (w2 `1)) by A5, A10, EUCLID:52;
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; :: thesis: verum