let x be set ; :: thesis: for a, b, c, d being Real st x in rectangle (a,b,c,d) & a < b & c < d & not x in LSeg (|[a,c]|,|[a,d]|) & not x in LSeg (|[a,d]|,|[b,d]|) & not x in LSeg (|[b,d]|,|[b,c]|) holds
x in LSeg (|[b,c]|,|[a,c]|)
let a, b, c, d be Real; :: thesis: ( x in rectangle (a,b,c,d) & a < b & c < d & not x in LSeg (|[a,c]|,|[a,d]|) & not x in LSeg (|[a,d]|,|[b,d]|) & not x in LSeg (|[b,d]|,|[b,c]|) implies x in LSeg (|[b,c]|,|[a,c]|) )
assume that
A1: x in rectangle (a,b,c,d) and
A2: a < b and
A3: c < d ; :: thesis: ( x in LSeg (|[a,c]|,|[a,d]|) or x in LSeg (|[a,d]|,|[b,d]|) or x in LSeg (|[b,d]|,|[b,c]|) or x in LSeg (|[b,c]|,|[a,c]|) )
x in { q where q is Point of (TOP-REAL 2) : ( ( q `1 = a & q `2 <= d & q `2 >= c ) or ( q `1 <= b & q `1 >= a & q `2 = d ) or ( q `1 <= b & q `1 >= a & q `2 = c ) or ( q `1 = b & q `2 <= d & q `2 >= c ) ) } by A1, A2, A3, SPPOL_2:54;
then consider p being Point of (TOP-REAL 2) such that
A4: p = x and
A5: ( ( p `1 = a & p `2 <= d & p `2 >= c ) or ( p `1 <= b & p `1 >= a & p `2 = d ) or ( p `1 <= b & p `1 >= a & p `2 = c ) or ( p `1 = b & p `2 <= d & p `2 >= c ) ) ;
now :: thesis: ( ( p `1 = a & c <= p `2 & p `2 <= d & ( x in LSeg (|[a,c]|,|[a,d]|) or x in LSeg (|[a,d]|,|[b,d]|) or x in LSeg (|[b,d]|,|[b,c]|) or x in LSeg (|[b,c]|,|[a,c]|) ) ) or ( p `2 = d & a <= p `1 & p `1 <= b & ( x in LSeg (|[a,c]|,|[a,d]|) or x in LSeg (|[a,d]|,|[b,d]|) or x in LSeg (|[b,d]|,|[b,c]|) or x in LSeg (|[b,c]|,|[a,c]|) ) ) or ( p `1 = b & c <= p `2 & p `2 <= d & ( x in LSeg (|[a,c]|,|[a,d]|) or x in LSeg (|[a,d]|,|[b,d]|) or x in LSeg (|[b,d]|,|[b,c]|) or x in LSeg (|[b,c]|,|[a,c]|) ) ) or ( p `2 = c & a <= p `1 & p `1 <= b & ( x in LSeg (|[a,c]|,|[a,d]|) or x in LSeg (|[a,d]|,|[b,d]|) or x in LSeg (|[b,d]|,|[b,c]|) or x in LSeg (|[b,c]|,|[a,c]|) ) ) )
per cases ( ( p `1 = a & c <= p `2 & p `2 <= d ) or ( p `2 = d & a <= p `1 & p `1 <= b ) or ( p `1 = b & c <= p `2 & p `2 <= d ) or ( p `2 = c & a <= p `1 & p `1 <= b ) ) by A5;
case A6: ( p `1 = a & c <= p `2 & p `2 <= d ) ; :: thesis: ( x in LSeg (|[a,c]|,|[a,d]|) or x in LSeg (|[a,d]|,|[b,d]|) or x in LSeg (|[b,d]|,|[b,c]|) or x in LSeg (|[b,c]|,|[a,c]|) )
A7: d - c > 0 by A3, XREAL_1:50;
A8: (p `2) - c >= 0 by A6, XREAL_1:48;
A9: d - (p `2) >= 0 by A6, XREAL_1:48;
reconsider r = ((p `2) - c) / (d - c) as Real ;
A10: 1 - r = ((d - c) / (d - c)) - (((p `2) - c) / (d - c)) by A7, XCMPLX_1:60
.= ((d - c) - ((p `2) - c)) / (d - c) by XCMPLX_1:120
.= (d - (p `2)) / (d - c) ;
then A11: (1 - r) + r >= 0 + r by A7, A9, XREAL_1:7;
A12: (((1 - r) * |[a,c]|) + (r * |[a,d]|)) `1 = (((1 - r) * |[a,c]|) `1) + ((r * |[a,d]|) `1) by TOPREAL3:2
.= ((1 - r) * (|[a,c]| `1)) + ((r * |[a,d]|) `1) by TOPREAL3:4
.= ((1 - r) * a) + ((r * |[a,d]|) `1) by EUCLID:52
.= ((1 - r) * a) + (r * (|[a,d]| `1)) by TOPREAL3:4
.= ((1 - r) * a) + (r * a) by EUCLID:52
.= p `1 by A6 ;
(((1 - r) * |[a,c]|) + (r * |[a,d]|)) `2 = (((1 - r) * |[a,c]|) `2) + ((r * |[a,d]|) `2) by TOPREAL3:2
.= ((1 - r) * (|[a,c]| `2)) + ((r * |[a,d]|) `2) by TOPREAL3:4
.= ((1 - r) * c) + ((r * |[a,d]|) `2) by EUCLID:52
.= ((1 - r) * c) + (r * (|[a,d]| `2)) by TOPREAL3:4
.= (((d - (p `2)) / (d - c)) * c) + ((((p `2) - c) / (d - c)) * d) by A10, EUCLID:52
.= (((d - (p `2)) * ((d - c) ")) * c) + ((((p `2) - c) / (d - c)) * d) by XCMPLX_0:def 9
.= (((d - c) ") * ((d - (p `2)) * c)) + ((((d - c) ") * ((p `2) - c)) * d) by XCMPLX_0:def 9
.= (((d - c) ") * (d - c)) * (p `2)
.= 1 * (p `2) by A7, XCMPLX_0:def 7
.= p `2 ;
then p = |[((((1 - r) * |[a,c]|) + (r * |[a,d]|)) `1),((((1 - r) * |[a,c]|) + (r * |[a,d]|)) `2)]| by A12, EUCLID:53
.= ((1 - r) * |[a,c]|) + (r * |[a,d]|) by EUCLID:53 ;
hence ( x in LSeg (|[a,c]|,|[a,d]|) or x in LSeg (|[a,d]|,|[b,d]|) or x in LSeg (|[b,d]|,|[b,c]|) or x in LSeg (|[b,c]|,|[a,c]|) ) by A4, A7, A8, A11; :: thesis: verum
end;
case A13: ( p `2 = d & a <= p `1 & p `1 <= b ) ; :: thesis: ( x in LSeg (|[a,c]|,|[a,d]|) or x in LSeg (|[a,d]|,|[b,d]|) or x in LSeg (|[b,d]|,|[b,c]|) or x in LSeg (|[b,c]|,|[a,c]|) )
A14: b - a > 0 by A2, XREAL_1:50;
A15: (p `1) - a >= 0 by A13, XREAL_1:48;
A16: b - (p `1) >= 0 by A13, XREAL_1:48;
reconsider r = ((p `1) - a) / (b - a) as Real ;
A17: 1 - r = ((b - a) / (b - a)) - (((p `1) - a) / (b - a)) by A14, XCMPLX_1:60
.= ((b - a) - ((p `1) - a)) / (b - a) by XCMPLX_1:120
.= (b - (p `1)) / (b - a) ;
then A18: (1 - r) + r >= 0 + r by A14, A16, XREAL_1:7;
A19: (((1 - r) * |[a,d]|) + (r * |[b,d]|)) `1 = (((1 - r) * |[a,d]|) `1) + ((r * |[b,d]|) `1) by TOPREAL3:2
.= ((1 - r) * (|[a,d]| `1)) + ((r * |[b,d]|) `1) by TOPREAL3:4
.= ((1 - r) * a) + ((r * |[b,d]|) `1) by EUCLID:52
.= ((1 - r) * a) + (r * (|[b,d]| `1)) by TOPREAL3:4
.= (((b - (p `1)) / (b - a)) * a) + ((((p `1) - a) / (b - a)) * b) by A17, EUCLID:52
.= (((b - (p `1)) * ((b - a) ")) * a) + ((((p `1) - a) / (b - a)) * b) by XCMPLX_0:def 9
.= (((b - a) ") * ((b - (p `1)) * a)) + ((((b - a) ") * ((p `1) - a)) * b) by XCMPLX_0:def 9
.= (((b - a) ") * (b - a)) * (p `1)
.= 1 * (p `1) by A14, XCMPLX_0:def 7
.= p `1 ;
(((1 - r) * |[a,d]|) + (r * |[b,d]|)) `2 = (((1 - r) * |[a,d]|) `2) + ((r * |[b,d]|) `2) by TOPREAL3:2
.= ((1 - r) * (|[a,d]| `2)) + ((r * |[b,d]|) `2) by TOPREAL3:4
.= ((1 - r) * d) + ((r * |[b,d]|) `2) by EUCLID:52
.= ((1 - r) * d) + (r * (|[b,d]| `2)) by TOPREAL3:4
.= ((1 - r) * d) + (r * d) by EUCLID:52
.= p `2 by A13 ;
then p = |[((((1 - r) * |[a,d]|) + (r * |[b,d]|)) `1),((((1 - r) * |[a,d]|) + (r * |[b,d]|)) `2)]| by A19, EUCLID:53
.= ((1 - r) * |[a,d]|) + (r * |[b,d]|) by EUCLID:53 ;
hence ( x in LSeg (|[a,c]|,|[a,d]|) or x in LSeg (|[a,d]|,|[b,d]|) or x in LSeg (|[b,d]|,|[b,c]|) or x in LSeg (|[b,c]|,|[a,c]|) ) by A4, A14, A15, A18; :: thesis: verum
end;
case A20: ( p `1 = b & c <= p `2 & p `2 <= d ) ; :: thesis: ( x in LSeg (|[a,c]|,|[a,d]|) or x in LSeg (|[a,d]|,|[b,d]|) or x in LSeg (|[b,d]|,|[b,c]|) or x in LSeg (|[b,c]|,|[a,c]|) )
A21: d - c > 0 by A3, XREAL_1:50;
A22: (p `2) - c >= 0 by A20, XREAL_1:48;
A23: d - (p `2) >= 0 by A20, XREAL_1:48;
reconsider r = (d - (p `2)) / (d - c) as Real ;
A24: 1 - r = ((d - c) / (d - c)) - ((d - (p `2)) / (d - c)) by A21, XCMPLX_1:60
.= ((d - c) - (d - (p `2))) / (d - c) by XCMPLX_1:120
.= ((p `2) - c) / (d - c) ;
then A25: (1 - r) + r >= 0 + r by A21, A22, XREAL_1:7;
A26: (((1 - r) * |[b,d]|) + (r * |[b,c]|)) `1 = (((1 - r) * |[b,d]|) `1) + ((r * |[b,c]|) `1) by TOPREAL3:2
.= ((1 - r) * (|[b,d]| `1)) + ((r * |[b,c]|) `1) by TOPREAL3:4
.= ((1 - r) * b) + ((r * |[b,c]|) `1) by EUCLID:52
.= ((1 - r) * b) + (r * (|[b,c]| `1)) by TOPREAL3:4
.= ((1 - r) * b) + (r * b) by EUCLID:52
.= p `1 by A20 ;
(((1 - r) * |[b,d]|) + (r * |[b,c]|)) `2 = (((1 - r) * |[b,d]|) `2) + ((r * |[b,c]|) `2) by TOPREAL3:2
.= ((1 - r) * (|[b,d]| `2)) + ((r * |[b,c]|) `2) by TOPREAL3:4
.= ((1 - r) * d) + ((r * |[b,c]|) `2) by EUCLID:52
.= ((1 - r) * d) + (r * (|[b,c]| `2)) by TOPREAL3:4
.= ((((p `2) - c) / (d - c)) * d) + (((d - (p `2)) / (d - c)) * c) by A24, EUCLID:52
.= ((((p `2) - c) * ((d - c) ")) * d) + (((d - (p `2)) / (d - c)) * c) by XCMPLX_0:def 9
.= (((d - c) ") * (((p `2) - c) * d)) + ((((d - c) ") * (d - (p `2))) * c) by XCMPLX_0:def 9
.= (((d - c) ") * (d - c)) * (p `2)
.= 1 * (p `2) by A21, XCMPLX_0:def 7
.= p `2 ;
then p = |[((((1 - r) * |[b,d]|) + (r * |[b,c]|)) `1),((((1 - r) * |[b,d]|) + (r * |[b,c]|)) `2)]| by A26, EUCLID:53
.= ((1 - r) * |[b,d]|) + (r * |[b,c]|) by EUCLID:53 ;
hence ( x in LSeg (|[a,c]|,|[a,d]|) or x in LSeg (|[a,d]|,|[b,d]|) or x in LSeg (|[b,d]|,|[b,c]|) or x in LSeg (|[b,c]|,|[a,c]|) ) by A4, A21, A23, A25; :: thesis: verum
end;
case A27: ( p `2 = c & a <= p `1 & p `1 <= b ) ; :: thesis: ( x in LSeg (|[a,c]|,|[a,d]|) or x in LSeg (|[a,d]|,|[b,d]|) or x in LSeg (|[b,d]|,|[b,c]|) or x in LSeg (|[b,c]|,|[a,c]|) )
A28: b - a > 0 by A2, XREAL_1:50;
A29: (p `1) - a >= 0 by A27, XREAL_1:48;
A30: b - (p `1) >= 0 by A27, XREAL_1:48;
reconsider r = (b - (p `1)) / (b - a) as Real ;
A31: 1 - r = ((b - a) / (b - a)) - ((b - (p `1)) / (b - a)) by A28, XCMPLX_1:60
.= ((b - a) - (b - (p `1))) / (b - a) by XCMPLX_1:120
.= ((p `1) - a) / (b - a) ;
then A32: (1 - r) + r >= 0 + r by A28, A29, XREAL_1:7;
A33: (((1 - r) * |[b,c]|) + (r * |[a,c]|)) `1 = (((1 - r) * |[b,c]|) `1) + ((r * |[a,c]|) `1) by TOPREAL3:2
.= ((1 - r) * (|[b,c]| `1)) + ((r * |[a,c]|) `1) by TOPREAL3:4
.= ((1 - r) * b) + ((r * |[a,c]|) `1) by EUCLID:52
.= ((1 - r) * b) + (r * (|[a,c]| `1)) by TOPREAL3:4
.= ((((p `1) - a) / (b - a)) * b) + (((b - (p `1)) / (b - a)) * a) by A31, EUCLID:52
.= ((((p `1) - a) * ((b - a) ")) * b) + (((b - (p `1)) / (b - a)) * a) by XCMPLX_0:def 9
.= (((b - a) ") * (((p `1) - a) * b)) + ((((b - a) ") * (b - (p `1))) * a) by XCMPLX_0:def 9
.= (((b - a) ") * (b - a)) * (p `1)
.= 1 * (p `1) by A28, XCMPLX_0:def 7
.= p `1 ;
(((1 - r) * |[b,c]|) + (r * |[a,c]|)) `2 = (((1 - r) * |[b,c]|) `2) + ((r * |[a,c]|) `2) by TOPREAL3:2
.= ((1 - r) * (|[b,c]| `2)) + ((r * |[a,c]|) `2) by TOPREAL3:4
.= ((1 - r) * c) + ((r * |[a,c]|) `2) by EUCLID:52
.= ((1 - r) * c) + (r * (|[a,c]| `2)) by TOPREAL3:4
.= ((1 - r) * c) + (r * c) by EUCLID:52
.= p `2 by A27 ;
then p = |[((((1 - r) * |[b,c]|) + (r * |[a,c]|)) `1),((((1 - r) * |[b,c]|) + (r * |[a,c]|)) `2)]| by A33, EUCLID:53
.= ((1 - r) * |[b,c]|) + (r * |[a,c]|) by EUCLID:53 ;
hence ( x in LSeg (|[a,c]|,|[a,d]|) or x in LSeg (|[a,d]|,|[b,d]|) or x in LSeg (|[b,d]|,|[b,c]|) or x in LSeg (|[b,c]|,|[a,c]|) ) by A4, A28, A30, A32; :: thesis: verum
end;
end;
end;
hence ( x in LSeg (|[a,c]|,|[a,d]|) or x in LSeg (|[a,d]|,|[b,d]|) or x in LSeg (|[b,d]|,|[b,c]|) or x in LSeg (|[b,c]|,|[a,c]|) ) ; :: thesis: verum