let x be set ; :: thesis: for a, b, c, d being real number 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 number ; :: 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 A1: ( x in rectangle a,b,c,d & a < b & 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]| )
then 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 SPPOL_2:58;
then consider p being Point of (TOP-REAL 2) such that
A2: ( p = x & ( ( 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

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 A2;

case A3: ( 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]| )

A4: d - c > 0 by A1, XREAL_1:52;
then A5: (d - c) " > 0 ;
A6: (p `2 ) - c >= 0 by A3, XREAL_1:50;
A7: d - (p `2 ) >= 0 by A3, XREAL_1:50;
((p `2 ) - c) / (d - c) = ((p `2 ) - c) * ((d - c) " ) by XCMPLX_0:def 9;
then A8: ((p `2 ) - c) / (d - c) >= 0 by A5, A6;
reconsider r = ((p `2 ) - c) / (d - c) as Real ;
A9: 1 - r = ((d - c) / (d - c)) - (((p `2 ) - c) / (d - c)) by A4, XCMPLX_1:60
.= ((d - c) - ((p `2 ) - c)) / (d - c) by XCMPLX_1:121
.= (d - (p `2 )) / (d - c) ;
then 1 - r = (d - (p `2 )) * ((d - c) " ) by XCMPLX_0:def 9;
then 1 - r >= 0 by A5, A7;
then A10: (1 - r) + r >= 0 + r by XREAL_1:9;
A11: (((1 - r) * |[a,c]|) + (r * |[a,d]|)) `1 = (((1 - r) * |[a,c]|) `1 ) + ((r * |[a,d]|) `1 ) by TOPREAL3:7
.= ((1 - r) * (|[a,c]| `1 )) + ((r * |[a,d]|) `1 ) by TOPREAL3:9
.= ((1 - r) * a) + ((r * |[a,d]|) `1 ) by EUCLID:56
.= ((1 - r) * a) + (r * (|[a,d]| `1 )) by TOPREAL3:9
.= ((1 - r) * a) + (r * a) by EUCLID:56
.= p `1 by A3 ;
(((1 - r) * |[a,c]|) + (r * |[a,d]|)) `2 = (((1 - r) * |[a,c]|) `2 ) + ((r * |[a,d]|) `2 ) by TOPREAL3:7
.= ((1 - r) * (|[a,c]| `2 )) + ((r * |[a,d]|) `2 ) by TOPREAL3:9
.= ((1 - r) * c) + ((r * |[a,d]|) `2 ) by EUCLID:56
.= ((1 - r) * c) + (r * (|[a,d]| `2 )) by TOPREAL3:9
.= (((d - (p `2 )) / (d - c)) * c) + ((((p `2 ) - c) / (d - c)) * d) by A9, EUCLID:56
.= (((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 A4, 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 A11, EUCLID:57
.= ((1 - r) * |[a,c]|) + (r * |[a,d]|) by EUCLID:57 ;
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 A2, A8, A10; :: thesis: verum

end;

case A12: ( 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]| )

A13: b - a > 0 by A1, XREAL_1:52;
then A14: (b - a) " > 0 ;
A15: (p `1 ) - a >= 0 by A12, XREAL_1:50;
A16: b - (p `1 ) >= 0 by A12, XREAL_1:50;
((p `1 ) - a) / (b - a) = ((p `1 ) - a) * ((b - a) " ) by XCMPLX_0:def 9;
then A17: ((p `1 ) - a) / (b - a) >= 0 by A14, A15;
reconsider r = ((p `1 ) - a) / (b - a) as Real ;
A18: 1 - r = ((b - a) / (b - a)) - (((p `1 ) - a) / (b - a)) by A13, XCMPLX_1:60
.= ((b - a) - ((p `1 ) - a)) / (b - a) by XCMPLX_1:121
.= (b - (p `1 )) / (b - a) ;
then 1 - r = (b - (p `1 )) * ((b - a) " ) by XCMPLX_0:def 9;
then 1 - r >= 0 by A14, A16;
then A19: (1 - r) + r >= 0 + r by XREAL_1:9;
A20: (((1 - r) * |[a,d]|) + (r * |[b,d]|)) `1 = (((1 - r) * |[a,d]|) `1 ) + ((r * |[b,d]|) `1 ) by TOPREAL3:7
.= ((1 - r) * (|[a,d]| `1 )) + ((r * |[b,d]|) `1 ) by TOPREAL3:9
.= ((1 - r) * a) + ((r * |[b,d]|) `1 ) by EUCLID:56
.= ((1 - r) * a) + (r * (|[b,d]| `1 )) by TOPREAL3:9
.= (((b - (p `1 )) / (b - a)) * a) + ((((p `1 ) - a) / (b - a)) * b) by A18, EUCLID:56
.= (((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 A13, 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:7
.= ((1 - r) * (|[a,d]| `2 )) + ((r * |[b,d]|) `2 ) by TOPREAL3:9
.= ((1 - r) * d) + ((r * |[b,d]|) `2 ) by EUCLID:56
.= ((1 - r) * d) + (r * (|[b,d]| `2 )) by TOPREAL3:9
.= ((1 - r) * d) + (r * d) by EUCLID:56
.= p `2 by A12 ;
then p = |[((((1 - r) * |[a,d]|) + (r * |[b,d]|)) `1 ),((((1 - r) * |[a,d]|) + (r * |[b,d]|)) `2 )]| by A20, EUCLID:57
.= ((1 - r) * |[a,d]|) + (r * |[b,d]|) by EUCLID:57 ;
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 A2, A17, A19; :: thesis: verum

end;

case A21: ( 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]| )

A22: d - c > 0 by A1, XREAL_1:52;
then A23: (d - c) " > 0 ;
A24: (p `2 ) - c >= 0 by A21, XREAL_1:50;
A25: d - (p `2 ) >= 0 by A21, XREAL_1:50;
(d - (p `2 )) / (d - c) = (d - (p `2 )) * ((d - c) " ) by XCMPLX_0:def 9;
then A26: (d - (p `2 )) / (d - c) >= 0 by A23, A25;
reconsider r = (d - (p `2 )) / (d - c) as Real ;
A27: 1 - r = ((d - c) / (d - c)) - ((d - (p `2 )) / (d - c)) by A22, XCMPLX_1:60
.= ((d - c) - (d - (p `2 ))) / (d - c) by XCMPLX_1:121
.= ((p `2 ) - c) / (d - c) ;
then 1 - r = ((p `2 ) - c) * ((d - c) " ) by XCMPLX_0:def 9;
then 1 - r >= 0 by A23, A24;
then A28: (1 - r) + r >= 0 + r by XREAL_1:9;
A29: (((1 - r) * |[b,d]|) + (r * |[b,c]|)) `1 = (((1 - r) * |[b,d]|) `1 ) + ((r * |[b,c]|) `1 ) by TOPREAL3:7
.= ((1 - r) * (|[b,d]| `1 )) + ((r * |[b,c]|) `1 ) by TOPREAL3:9
.= ((1 - r) * b) + ((r * |[b,c]|) `1 ) by EUCLID:56
.= ((1 - r) * b) + (r * (|[b,c]| `1 )) by TOPREAL3:9
.= ((1 - r) * b) + (r * b) by EUCLID:56
.= p `1 by A21 ;
(((1 - r) * |[b,d]|) + (r * |[b,c]|)) `2 = (((1 - r) * |[b,d]|) `2 ) + ((r * |[b,c]|) `2 ) by TOPREAL3:7
.= ((1 - r) * (|[b,d]| `2 )) + ((r * |[b,c]|) `2 ) by TOPREAL3:9
.= ((1 - r) * d) + ((r * |[b,c]|) `2 ) by EUCLID:56
.= ((1 - r) * d) + (r * (|[b,c]| `2 )) by TOPREAL3:9
.= ((((p `2 ) - c) / (d - c)) * d) + (((d - (p `2 )) / (d - c)) * c) by A27, EUCLID:56
.= ((((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 A22, 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 A29, EUCLID:57
.= ((1 - r) * |[b,d]|) + (r * |[b,c]|) by EUCLID:57 ;
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 A2, A26, A28; :: thesis: verum

end;

case A30: ( 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]| )

A31: b - a > 0 by A1, XREAL_1:52;
then A32: (b - a) " > 0 ;
A33: (p `1 ) - a >= 0 by A30, XREAL_1:50;
A34: b - (p `1 ) >= 0 by A30, XREAL_1:50;
(b - (p `1 )) / (b - a) = (b - (p `1 )) * ((b - a) " ) by XCMPLX_0:def 9;
then A35: (b - (p `1 )) / (b - a) >= 0 by A32, A34;
reconsider r = (b - (p `1 )) / (b - a) as Real ;
A36: 1 - r = ((b - a) / (b - a)) - ((b - (p `1 )) / (b - a)) by A31, XCMPLX_1:60
.= ((b - a) - (b - (p `1 ))) / (b - a) by XCMPLX_1:121
.= ((p `1 ) - a) / (b - a) ;
then 1 - r = ((p `1 ) - a) * ((b - a) " ) by XCMPLX_0:def 9;
then 1 - r >= 0 by A32, A33;
then A37: (1 - r) + r >= 0 + r by XREAL_1:9;
A38: (((1 - r) * |[b,c]|) + (r * |[a,c]|)) `1 = (((1 - r) * |[b,c]|) `1 ) + ((r * |[a,c]|) `1 ) by TOPREAL3:7
.= ((1 - r) * (|[b,c]| `1 )) + ((r * |[a,c]|) `1 ) by TOPREAL3:9
.= ((1 - r) * b) + ((r * |[a,c]|) `1 ) by EUCLID:56
.= ((1 - r) * b) + (r * (|[a,c]| `1 )) by TOPREAL3:9
.= ((((p `1 ) - a) / (b - a)) * b) + (((b - (p `1 )) / (b - a)) * a) by A36, EUCLID:56
.= ((((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 A31, 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:7
.= ((1 - r) * (|[b,c]| `2 )) + ((r * |[a,c]|) `2 ) by TOPREAL3:9
.= ((1 - r) * c) + ((r * |[a,c]|) `2 ) by EUCLID:56
.= ((1 - r) * c) + (r * (|[a,c]| `2 )) by TOPREAL3:9
.= ((1 - r) * c) + (r * c) by EUCLID:56
.= p `2 by A30 ;
then p = |[((((1 - r) * |[b,c]|) + (r * |[a,c]|)) `1 ),((((1 - r) * |[b,c]|) + (r * |[a,c]|)) `2 )]| by A38, EUCLID:57
.= ((1 - r) * |[b,c]|) + (r * |[a,c]|) by EUCLID:57 ;
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 A2, A35, A37; :: 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