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 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:58;
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

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:52;
A8: (p `2 ) - c >= 0 by A6, XREAL_1:50;
A9: d - (p `2 ) >= 0 by A6, XREAL_1:50;
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:121
.= (d - (p `2 )) / (d - c) ;
then A11: (1 - r) + r >= 0 + r by A7, A9, XREAL_1:9;
A12: (((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 A6 ;
(((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 A10, 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 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: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 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:52;
A15: (p `1 ) - a >= 0 by A13, XREAL_1:50;
A16: b - (p `1 ) >= 0 by A13, XREAL_1:50;
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:121
.= (b - (p `1 )) / (b - a) ;
then A18: (1 - r) + r >= 0 + r by A14, A16, XREAL_1:9;
A19: (((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 A17, 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 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: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 A13 ;
then p = |[((((1 - r) * |[a,d]|) + (r * |[b,d]|)) `1 ),((((1 - r) * |[a,d]|) + (r * |[b,d]|)) `2 )]| by A19, 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 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:52;
A22: (p `2 ) - c >= 0 by A20, XREAL_1:50;
A23: d - (p `2 ) >= 0 by A20, XREAL_1:50;
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:121
.= ((p `2 ) - c) / (d - c) ;
then A25: (1 - r) + r >= 0 + r by A21, A22, XREAL_1:9;
A26: (((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 A20 ;
(((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 A24, 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 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: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 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:52;
A29: (p `1 ) - a >= 0 by A27, XREAL_1:50;
A30: b - (p `1 ) >= 0 by A27, XREAL_1:50;
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:121
.= ((p `1 ) - a) / (b - a) ;
then A32: (1 - r) + r >= 0 + r by A28, A29, XREAL_1:9;
A33: (((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 A31, 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 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: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 A27 ;
then p = |[((((1 - r) * |[b,c]|) + (r * |[a,c]|)) `1 ),((((1 - r) * |[b,c]|) + (r * |[a,c]|)) `2 )]| by A33, 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 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