let x be set ; 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; ( 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
; ( 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 ( ( 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 )
;
( 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;
verum end; case A13:
(
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]|) )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;
verum end; case A20:
(
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]|) )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;
verum end; case A27:
(
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]|) )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;
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]|) )
; verum