let a, b, c, d be Real; ( a <= b & c <= d implies ( LSeg (|[a,c]|,|[a,d]|) = { p1 where p1 is Point of (TOP-REAL 2) : ( p1 `1 = a & p1 `2 <= d & p1 `2 >= c ) } & LSeg (|[a,d]|,|[b,d]|) = { p2 where p2 is Point of (TOP-REAL 2) : ( p2 `1 <= b & p2 `1 >= a & p2 `2 = d ) } & LSeg (|[a,c]|,|[b,c]|) = { q1 where q1 is Point of (TOP-REAL 2) : ( q1 `1 <= b & q1 `1 >= a & q1 `2 = c ) } & LSeg (|[b,c]|,|[b,d]|) = { q2 where q2 is Point of (TOP-REAL 2) : ( q2 `1 = b & q2 `2 <= d & q2 `2 >= c ) } ) )
assume that
A1:
a <= b
and
A2:
c <= d
; ( LSeg (|[a,c]|,|[a,d]|) = { p1 where p1 is Point of (TOP-REAL 2) : ( p1 `1 = a & p1 `2 <= d & p1 `2 >= c ) } & LSeg (|[a,d]|,|[b,d]|) = { p2 where p2 is Point of (TOP-REAL 2) : ( p2 `1 <= b & p2 `1 >= a & p2 `2 = d ) } & LSeg (|[a,c]|,|[b,c]|) = { q1 where q1 is Point of (TOP-REAL 2) : ( q1 `1 <= b & q1 `1 >= a & q1 `2 = c ) } & LSeg (|[b,c]|,|[b,d]|) = { q2 where q2 is Point of (TOP-REAL 2) : ( q2 `1 = b & q2 `2 <= d & q2 `2 >= c ) } )
set L1 = { p where p is Point of (TOP-REAL 2) : ( p `1 = a & p `2 <= d & p `2 >= c ) } ;
set L2 = { p where p is Point of (TOP-REAL 2) : ( p `1 <= b & p `1 >= a & p `2 = d ) } ;
set L3 = { p where p is Point of (TOP-REAL 2) : ( p `1 <= b & p `1 >= a & p `2 = c ) } ;
set L4 = { p where p is Point of (TOP-REAL 2) : ( p `1 = b & p `2 <= d & p `2 >= c ) } ;
set p0 = |[a,c]|;
set p01 = |[a,d]|;
set p10 = |[b,c]|;
set p1 = |[b,d]|;
A3:
|[a,d]| `1 = a
by EUCLID:52;
A4:
|[a,d]| `2 = d
by EUCLID:52;
A5:
|[b,c]| `1 = b
by EUCLID:52;
A6:
|[b,c]| `2 = c
by EUCLID:52;
A7:
{ p where p is Point of (TOP-REAL 2) : ( p `1 = a & p `2 <= d & p `2 >= c ) } c= LSeg (|[a,c]|,|[a,d]|)
proof
let a2 be
object ;
TARSKI:def 3 ( not a2 in { p where p is Point of (TOP-REAL 2) : ( p `1 = a & p `2 <= d & p `2 >= c ) } or a2 in LSeg (|[a,c]|,|[a,d]|) )
assume
a2 in { p where p is Point of (TOP-REAL 2) : ( p `1 = a & p `2 <= d & p `2 >= c ) }
;
a2 in LSeg (|[a,c]|,|[a,d]|)
then consider p being
Point of
(TOP-REAL 2) such that A8:
a2 = p
and A9:
p `1 = a
and A10:
p `2 <= d
and A11:
p `2 >= c
;
now ( ( d <> c & a2 in LSeg (|[a,c]|,|[a,d]|) ) or ( d = c & a2 in LSeg (|[a,c]|,|[a,d]|) ) )per cases
( d <> c or d = c )
;
case A12:
d <> c
;
a2 in LSeg (|[a,c]|,|[a,d]|)reconsider lambda =
((p `2) - c) / (d - c) as
Real ;
d >= c
by A10, A11, XXREAL_0:2;
then
d > c
by A12, XXREAL_0:1;
then A13:
d - c > 0
by XREAL_1:50;
A14:
(p `2) - c >= 0
by A11, XREAL_1:48;
d - c >= (p `2) - c
by A10, XREAL_1:9;
then
(d - c) / (d - c) >= ((p `2) - c) / (d - c)
by A13, XREAL_1:72;
then A15:
1
>= lambda
by A13, XCMPLX_1:60;
A16:
((1 - lambda) * c) + (lambda * d) =
((((d - c) / (d - c)) - (((p `2) - c) / (d - c))) * c) + ((((p `2) - c) / (d - c)) * d)
by A13, XCMPLX_1:60
.=
((((d - c) - ((p `2) - c)) / (d - c)) * c) + ((((p `2) - c) / (d - c)) * d)
by XCMPLX_1:120
.=
(c * ((d - (p `2)) / (d - c))) + ((d * ((p `2) - c)) / (d - c))
by XCMPLX_1:74
.=
((c * (d - (p `2))) / (d - c)) + ((d * ((p `2) - c)) / (d - c))
by XCMPLX_1:74
.=
(((c * d) - (c * (p `2))) + ((d * (p `2)) - (d * c))) / (d - c)
by XCMPLX_1:62
.=
((d - c) * (p `2)) / (d - c)
.=
(p `2) * ((d - c) / (d - c))
by XCMPLX_1:74
.=
(p `2) * 1
by A13, XCMPLX_1:60
.=
p `2
;
((1 - lambda) * |[a,c]|) + (lambda * |[a,d]|) =
|[((1 - lambda) * a),((1 - lambda) * c)]| + (lambda * |[a,d]|)
by EUCLID:58
.=
|[((1 - lambda) * a),((1 - lambda) * c)]| + |[(lambda * a),(lambda * d)]|
by EUCLID:58
.=
|[(((1 - lambda) * a) + (lambda * a)),(((1 - lambda) * c) + (lambda * d))]|
by EUCLID:56
.=
p
by A9, A16, EUCLID:53
;
hence
a2 in LSeg (
|[a,c]|,
|[a,d]|)
by A8, A13, A14, A15;
verum end; case
d = c
;
a2 in LSeg (|[a,c]|,|[a,d]|)then A17:
p `2 = c
by A10, A11, XXREAL_0:1;
reconsider lambda =
0 as
Real ;
((1 - lambda) * |[a,c]|) + (lambda * |[a,d]|) =
|[((1 - lambda) * a),((1 - lambda) * c)]| + (lambda * |[a,d]|)
by EUCLID:58
.=
|[((1 - lambda) * a),((1 - lambda) * c)]| + |[(lambda * a),(lambda * d)]|
by EUCLID:58
.=
|[(((1 - lambda) * a) + (lambda * a)),(((1 - lambda) * c) + (lambda * d))]|
by EUCLID:56
.=
p
by A9, A17, EUCLID:53
;
hence
a2 in LSeg (
|[a,c]|,
|[a,d]|)
by A8;
verum end;
hence
a2 in LSeg (
|[a,c]|,
|[a,d]|)
;
verum
end;
LSeg (|[a,c]|,|[a,d]|) c= { p where p is Point of (TOP-REAL 2) : ( p `1 = a & p `2 <= d & p `2 >= c ) }
proof
let a2 be
object ;
TARSKI:def 3 ( not a2 in LSeg (|[a,c]|,|[a,d]|) or a2 in { p where p is Point of (TOP-REAL 2) : ( p `1 = a & p `2 <= d & p `2 >= c ) } )
assume
a2 in LSeg (
|[a,c]|,
|[a,d]|)
;
a2 in { p where p is Point of (TOP-REAL 2) : ( p `1 = a & p `2 <= d & p `2 >= c ) }
then consider lambda being
Real such that A18:
a2 = ((1 - lambda) * |[a,c]|) + (lambda * |[a,d]|)
and A19:
0 <= lambda
and A20:
lambda <= 1
;
set q =
((1 - lambda) * |[a,c]|) + (lambda * |[a,d]|);
A21:
(((1 - lambda) * |[a,c]|) + (lambda * |[a,d]|)) `1 =
(((1 - lambda) * |[a,c]|) `1) + ((lambda * |[a,d]|) `1)
by TOPREAL3:2
.=
((1 - lambda) * (|[a,c]| `1)) + ((lambda * |[a,d]|) `1)
by TOPREAL3:4
.=
((1 - lambda) * (|[a,c]| `1)) + (lambda * (|[a,d]| `1))
by TOPREAL3:4
.=
((1 - lambda) * a) + (lambda * a)
by A3, EUCLID:52
.=
a
;
A22:
(((1 - lambda) * |[a,c]|) + (lambda * |[a,d]|)) `2 =
(((1 - lambda) * |[a,c]|) `2) + ((lambda * |[a,d]|) `2)
by TOPREAL3:2
.=
((1 - lambda) * (|[a,c]| `2)) + ((lambda * |[a,d]|) `2)
by TOPREAL3:4
.=
((1 - lambda) * (|[a,c]| `2)) + (lambda * (|[a,d]| `2))
by TOPREAL3:4
.=
((1 - lambda) * c) + (lambda * d)
by A4, EUCLID:52
;
then A23:
(((1 - lambda) * |[a,c]|) + (lambda * |[a,d]|)) `2 <= d
by A2, A20, XREAL_1:172;
(((1 - lambda) * |[a,c]|) + (lambda * |[a,d]|)) `2 >= c
by A2, A19, A20, A22, XREAL_1:173;
hence
a2 in { p where p is Point of (TOP-REAL 2) : ( p `1 = a & p `2 <= d & p `2 >= c ) }
by A18, A21, A23;
verum
end;
hence
{ p where p is Point of (TOP-REAL 2) : ( p `1 = a & p `2 <= d & p `2 >= c ) } = LSeg (|[a,c]|,|[a,d]|)
by A7; ( LSeg (|[a,d]|,|[b,d]|) = { p2 where p2 is Point of (TOP-REAL 2) : ( p2 `1 <= b & p2 `1 >= a & p2 `2 = d ) } & LSeg (|[a,c]|,|[b,c]|) = { q1 where q1 is Point of (TOP-REAL 2) : ( q1 `1 <= b & q1 `1 >= a & q1 `2 = c ) } & LSeg (|[b,c]|,|[b,d]|) = { q2 where q2 is Point of (TOP-REAL 2) : ( q2 `1 = b & q2 `2 <= d & q2 `2 >= c ) } )
A24:
{ p where p is Point of (TOP-REAL 2) : ( p `1 <= b & p `1 >= a & p `2 = d ) } c= LSeg (|[a,d]|,|[b,d]|)
proof
let a2 be
object ;
TARSKI:def 3 ( not a2 in { p where p is Point of (TOP-REAL 2) : ( p `1 <= b & p `1 >= a & p `2 = d ) } or a2 in LSeg (|[a,d]|,|[b,d]|) )
assume
a2 in { p where p is Point of (TOP-REAL 2) : ( p `1 <= b & p `1 >= a & p `2 = d ) }
;
a2 in LSeg (|[a,d]|,|[b,d]|)
then consider p being
Point of
(TOP-REAL 2) such that A25:
a2 = p
and A26:
p `1 <= b
and A27:
p `1 >= a
and A28:
p `2 = d
;
now ( ( b <> a & a2 in LSeg (|[a,d]|,|[b,d]|) ) or ( b = a & a2 in LSeg (|[a,d]|,|[b,d]|) ) )per cases
( b <> a or b = a )
;
case A29:
b <> a
;
a2 in LSeg (|[a,d]|,|[b,d]|)reconsider lambda =
((p `1) - a) / (b - a) as
Real ;
b >= a
by A26, A27, XXREAL_0:2;
then
b > a
by A29, XXREAL_0:1;
then A30:
b - a > 0
by XREAL_1:50;
A31:
(p `1) - a >= 0
by A27, XREAL_1:48;
b - a >= (p `1) - a
by A26, XREAL_1:9;
then
(b - a) / (b - a) >= ((p `1) - a) / (b - a)
by A30, XREAL_1:72;
then A32:
1
>= lambda
by A30, XCMPLX_1:60;
A33:
((1 - lambda) * a) + (lambda * b) =
((((b - a) / (b - a)) - (((p `1) - a) / (b - a))) * a) + ((((p `1) - a) / (b - a)) * b)
by A30, XCMPLX_1:60
.=
((((b - a) - ((p `1) - a)) / (b - a)) * a) + ((((p `1) - a) / (b - a)) * b)
by XCMPLX_1:120
.=
(a * ((b - (p `1)) / (b - a))) + ((b * ((p `1) - a)) / (b - a))
by XCMPLX_1:74
.=
((a * (b - (p `1))) / (b - a)) + ((b * ((p `1) - a)) / (b - a))
by XCMPLX_1:74
.=
(((a * b) - (a * (p `1))) + ((b * (p `1)) - (b * a))) / (b - a)
by XCMPLX_1:62
.=
((b - a) * (p `1)) / (b - a)
.=
(p `1) * ((b - a) / (b - a))
by XCMPLX_1:74
.=
(p `1) * 1
by A30, XCMPLX_1:60
.=
p `1
;
((1 - lambda) * |[a,d]|) + (lambda * |[b,d]|) =
|[((1 - lambda) * a),((1 - lambda) * d)]| + (lambda * |[b,d]|)
by EUCLID:58
.=
|[((1 - lambda) * a),((1 - lambda) * d)]| + |[(lambda * b),(lambda * d)]|
by EUCLID:58
.=
|[(((1 - lambda) * a) + (lambda * b)),(((1 - lambda) * d) + (lambda * d))]|
by EUCLID:56
.=
p
by A28, A33, EUCLID:53
;
hence
a2 in LSeg (
|[a,d]|,
|[b,d]|)
by A25, A30, A31, A32;
verum end; case
b = a
;
a2 in LSeg (|[a,d]|,|[b,d]|)then A34:
p `1 = a
by A26, A27, XXREAL_0:1;
reconsider lambda =
0 as
Real ;
((1 - lambda) * |[a,d]|) + (lambda * |[b,d]|) =
|[((1 - lambda) * a),((1 - lambda) * d)]| + (lambda * |[b,d]|)
by EUCLID:58
.=
|[((1 - lambda) * a),((1 - lambda) * d)]| + |[(lambda * b),(lambda * d)]|
by EUCLID:58
.=
|[(((1 - lambda) * a) + (lambda * b)),(((1 - lambda) * d) + (lambda * d))]|
by EUCLID:56
.=
p
by A28, A34, EUCLID:53
;
hence
a2 in LSeg (
|[a,d]|,
|[b,d]|)
by A25;
verum end;
hence
a2 in LSeg (
|[a,d]|,
|[b,d]|)
;
verum
end;
LSeg (|[a,d]|,|[b,d]|) c= { p where p is Point of (TOP-REAL 2) : ( p `1 <= b & p `1 >= a & p `2 = d ) }
proof
let a2 be
object ;
TARSKI:def 3 ( not a2 in LSeg (|[a,d]|,|[b,d]|) or a2 in { p where p is Point of (TOP-REAL 2) : ( p `1 <= b & p `1 >= a & p `2 = d ) } )
assume
a2 in LSeg (
|[a,d]|,
|[b,d]|)
;
a2 in { p where p is Point of (TOP-REAL 2) : ( p `1 <= b & p `1 >= a & p `2 = d ) }
then consider lambda being
Real such that A35:
a2 = ((1 - lambda) * |[a,d]|) + (lambda * |[b,d]|)
and A36:
0 <= lambda
and A37:
lambda <= 1
;
set q =
((1 - lambda) * |[a,d]|) + (lambda * |[b,d]|);
A38:
(((1 - lambda) * |[a,d]|) + (lambda * |[b,d]|)) `2 =
(((1 - lambda) * |[a,d]|) `2) + ((lambda * |[b,d]|) `2)
by TOPREAL3:2
.=
((1 - lambda) * (|[a,d]| `2)) + ((lambda * |[b,d]|) `2)
by TOPREAL3:4
.=
((1 - lambda) * (|[a,d]| `2)) + (lambda * (|[b,d]| `2))
by TOPREAL3:4
.=
((1 - lambda) * d) + (lambda * d)
by A4, EUCLID:52
.=
d
;
A39:
(((1 - lambda) * |[a,d]|) + (lambda * |[b,d]|)) `1 =
(((1 - lambda) * |[a,d]|) `1) + ((lambda * |[b,d]|) `1)
by TOPREAL3:2
.=
((1 - lambda) * (|[a,d]| `1)) + ((lambda * |[b,d]|) `1)
by TOPREAL3:4
.=
((1 - lambda) * (|[a,d]| `1)) + (lambda * (|[b,d]| `1))
by TOPREAL3:4
.=
((1 - lambda) * a) + (lambda * b)
by A3, EUCLID:52
;
then A40:
(((1 - lambda) * |[a,d]|) + (lambda * |[b,d]|)) `1 <= b
by A1, A37, XREAL_1:172;
(((1 - lambda) * |[a,d]|) + (lambda * |[b,d]|)) `1 >= a
by A1, A36, A37, A39, XREAL_1:173;
hence
a2 in { p where p is Point of (TOP-REAL 2) : ( p `1 <= b & p `1 >= a & p `2 = d ) }
by A35, A38, A40;
verum
end;
hence
{ p where p is Point of (TOP-REAL 2) : ( p `1 <= b & p `1 >= a & p `2 = d ) } = LSeg (|[a,d]|,|[b,d]|)
by A24; ( LSeg (|[a,c]|,|[b,c]|) = { q1 where q1 is Point of (TOP-REAL 2) : ( q1 `1 <= b & q1 `1 >= a & q1 `2 = c ) } & LSeg (|[b,c]|,|[b,d]|) = { q2 where q2 is Point of (TOP-REAL 2) : ( q2 `1 = b & q2 `2 <= d & q2 `2 >= c ) } )
A41:
{ p where p is Point of (TOP-REAL 2) : ( p `1 <= b & p `1 >= a & p `2 = c ) } c= LSeg (|[a,c]|,|[b,c]|)
proof
let a2 be
object ;
TARSKI:def 3 ( not a2 in { p where p is Point of (TOP-REAL 2) : ( p `1 <= b & p `1 >= a & p `2 = c ) } or a2 in LSeg (|[a,c]|,|[b,c]|) )
assume
a2 in { p where p is Point of (TOP-REAL 2) : ( p `1 <= b & p `1 >= a & p `2 = c ) }
;
a2 in LSeg (|[a,c]|,|[b,c]|)
then consider p being
Point of
(TOP-REAL 2) such that A42:
a2 = p
and A43:
p `1 <= b
and A44:
p `1 >= a
and A45:
p `2 = c
;
now ( ( b <> a & a2 in LSeg (|[a,c]|,|[b,c]|) ) or ( b = a & a2 in LSeg (|[a,c]|,|[b,c]|) ) )per cases
( b <> a or b = a )
;
case A46:
b <> a
;
a2 in LSeg (|[a,c]|,|[b,c]|)reconsider lambda =
((p `1) - a) / (b - a) as
Real ;
b >= a
by A43, A44, XXREAL_0:2;
then
b > a
by A46, XXREAL_0:1;
then A47:
b - a > 0
by XREAL_1:50;
A48:
(p `1) - a >= 0
by A44, XREAL_1:48;
b - a >= (p `1) - a
by A43, XREAL_1:9;
then
(b - a) / (b - a) >= ((p `1) - a) / (b - a)
by A47, XREAL_1:72;
then A49:
1
>= lambda
by A47, XCMPLX_1:60;
A50:
((1 - lambda) * a) + (lambda * b) =
((((b - a) / (b - a)) - (((p `1) - a) / (b - a))) * a) + ((((p `1) - a) / (b - a)) * b)
by A47, XCMPLX_1:60
.=
((((b - a) - ((p `1) - a)) / (b - a)) * a) + ((((p `1) - a) / (b - a)) * b)
by XCMPLX_1:120
.=
(a * ((b - (p `1)) / (b - a))) + ((b * ((p `1) - a)) / (b - a))
by XCMPLX_1:74
.=
((a * (b - (p `1))) / (b - a)) + ((b * ((p `1) - a)) / (b - a))
by XCMPLX_1:74
.=
(((a * b) - (a * (p `1))) + ((b * (p `1)) - (b * a))) / (b - a)
by XCMPLX_1:62
.=
((b - a) * (p `1)) / (b - a)
.=
(p `1) * ((b - a) / (b - a))
by XCMPLX_1:74
.=
(p `1) * 1
by A47, XCMPLX_1:60
.=
p `1
;
((1 - lambda) * |[a,c]|) + (lambda * |[b,c]|) =
|[((1 - lambda) * a),((1 - lambda) * c)]| + (lambda * |[b,c]|)
by EUCLID:58
.=
|[((1 - lambda) * a),((1 - lambda) * c)]| + |[(lambda * b),(lambda * c)]|
by EUCLID:58
.=
|[(((1 - lambda) * a) + (lambda * b)),(((1 - lambda) * c) + (lambda * c))]|
by EUCLID:56
.=
p
by A45, A50, EUCLID:53
;
hence
a2 in LSeg (
|[a,c]|,
|[b,c]|)
by A42, A47, A48, A49;
verum end; case
b = a
;
a2 in LSeg (|[a,c]|,|[b,c]|)then A51:
p `1 = a
by A43, A44, XXREAL_0:1;
reconsider lambda =
0 as
Real ;
((1 - lambda) * |[a,c]|) + (lambda * |[b,c]|) =
|[((1 - lambda) * a),((1 - lambda) * c)]| + (lambda * |[b,c]|)
by EUCLID:58
.=
|[((1 - lambda) * a),((1 - lambda) * c)]| + |[(lambda * b),(lambda * c)]|
by EUCLID:58
.=
|[(((1 - lambda) * a) + (lambda * b)),(((1 - lambda) * c) + (lambda * c))]|
by EUCLID:56
.=
p
by A45, A51, EUCLID:53
;
hence
a2 in LSeg (
|[a,c]|,
|[b,c]|)
by A42;
verum end;
hence
a2 in LSeg (
|[a,c]|,
|[b,c]|)
;
verum
end;
LSeg (|[a,c]|,|[b,c]|) c= { p where p is Point of (TOP-REAL 2) : ( p `1 <= b & p `1 >= a & p `2 = c ) }
proof
let a2 be
object ;
TARSKI:def 3 ( not a2 in LSeg (|[a,c]|,|[b,c]|) or a2 in { p where p is Point of (TOP-REAL 2) : ( p `1 <= b & p `1 >= a & p `2 = c ) } )
assume
a2 in LSeg (
|[a,c]|,
|[b,c]|)
;
a2 in { p where p is Point of (TOP-REAL 2) : ( p `1 <= b & p `1 >= a & p `2 = c ) }
then consider lambda being
Real such that A52:
a2 = ((1 - lambda) * |[a,c]|) + (lambda * |[b,c]|)
and A53:
0 <= lambda
and A54:
lambda <= 1
;
set q =
((1 - lambda) * |[a,c]|) + (lambda * |[b,c]|);
A55:
(((1 - lambda) * |[a,c]|) + (lambda * |[b,c]|)) `2 =
(((1 - lambda) * |[a,c]|) `2) + ((lambda * |[b,c]|) `2)
by TOPREAL3:2
.=
((1 - lambda) * (|[a,c]| `2)) + ((lambda * |[b,c]|) `2)
by TOPREAL3:4
.=
((1 - lambda) * (|[a,c]| `2)) + (lambda * (|[b,c]| `2))
by TOPREAL3:4
.=
((1 - lambda) * c) + (lambda * c)
by A6, EUCLID:52
.=
c
;
A56:
(((1 - lambda) * |[a,c]|) + (lambda * |[b,c]|)) `1 =
(((1 - lambda) * |[a,c]|) `1) + ((lambda * |[b,c]|) `1)
by TOPREAL3:2
.=
((1 - lambda) * (|[a,c]| `1)) + ((lambda * |[b,c]|) `1)
by TOPREAL3:4
.=
((1 - lambda) * (|[a,c]| `1)) + (lambda * (|[b,c]| `1))
by TOPREAL3:4
.=
((1 - lambda) * a) + (lambda * b)
by A5, EUCLID:52
;
then A57:
(((1 - lambda) * |[a,c]|) + (lambda * |[b,c]|)) `1 <= b
by A1, A54, XREAL_1:172;
(((1 - lambda) * |[a,c]|) + (lambda * |[b,c]|)) `1 >= a
by A1, A53, A54, A56, XREAL_1:173;
hence
a2 in { p where p is Point of (TOP-REAL 2) : ( p `1 <= b & p `1 >= a & p `2 = c ) }
by A52, A55, A57;
verum
end;
hence
{ p where p is Point of (TOP-REAL 2) : ( p `1 <= b & p `1 >= a & p `2 = c ) } = LSeg (|[a,c]|,|[b,c]|)
by A41; LSeg (|[b,c]|,|[b,d]|) = { q2 where q2 is Point of (TOP-REAL 2) : ( q2 `1 = b & q2 `2 <= d & q2 `2 >= c ) }
A58:
{ p where p is Point of (TOP-REAL 2) : ( p `1 = b & p `2 <= d & p `2 >= c ) } c= LSeg (|[b,c]|,|[b,d]|)
proof
let a2 be
object ;
TARSKI:def 3 ( not a2 in { p where p is Point of (TOP-REAL 2) : ( p `1 = b & p `2 <= d & p `2 >= c ) } or a2 in LSeg (|[b,c]|,|[b,d]|) )
assume
a2 in { p where p is Point of (TOP-REAL 2) : ( p `1 = b & p `2 <= d & p `2 >= c ) }
;
a2 in LSeg (|[b,c]|,|[b,d]|)
then consider p being
Point of
(TOP-REAL 2) such that A59:
a2 = p
and A60:
p `1 = b
and A61:
p `2 <= d
and A62:
p `2 >= c
;
now ( ( d <> c & a2 in LSeg (|[b,c]|,|[b,d]|) ) or ( d = c & a2 in LSeg (|[b,c]|,|[b,d]|) ) )per cases
( d <> c or d = c )
;
case A63:
d <> c
;
a2 in LSeg (|[b,c]|,|[b,d]|)reconsider lambda =
((p `2) - c) / (d - c) as
Real ;
d >= c
by A61, A62, XXREAL_0:2;
then
d > c
by A63, XXREAL_0:1;
then A64:
d - c > 0
by XREAL_1:50;
A65:
(p `2) - c >= 0
by A62, XREAL_1:48;
d - c >= (p `2) - c
by A61, XREAL_1:9;
then
(d - c) / (d - c) >= ((p `2) - c) / (d - c)
by A64, XREAL_1:72;
then A66:
1
>= lambda
by A64, XCMPLX_1:60;
A67:
((1 - lambda) * c) + (lambda * d) =
((((d - c) / (d - c)) - (((p `2) - c) / (d - c))) * c) + ((((p `2) - c) / (d - c)) * d)
by A64, XCMPLX_1:60
.=
((((d - c) - ((p `2) - c)) / (d - c)) * c) + ((((p `2) - c) / (d - c)) * d)
by XCMPLX_1:120
.=
(c * ((d - (p `2)) / (d - c))) + ((d * ((p `2) - c)) / (d - c))
by XCMPLX_1:74
.=
((c * (d - (p `2))) / (d - c)) + ((d * ((p `2) - c)) / (d - c))
by XCMPLX_1:74
.=
(((c * d) - (c * (p `2))) + ((d * (p `2)) - (d * c))) / (d - c)
by XCMPLX_1:62
.=
((d - c) * (p `2)) / (d - c)
.=
(p `2) * ((d - c) / (d - c))
by XCMPLX_1:74
.=
(p `2) * 1
by A64, XCMPLX_1:60
.=
p `2
;
((1 - lambda) * |[b,c]|) + (lambda * |[b,d]|) =
|[((1 - lambda) * b),((1 - lambda) * c)]| + (lambda * |[b,d]|)
by EUCLID:58
.=
|[((1 - lambda) * b),((1 - lambda) * c)]| + |[(lambda * b),(lambda * d)]|
by EUCLID:58
.=
|[(((1 - lambda) * b) + (lambda * b)),(((1 - lambda) * c) + (lambda * d))]|
by EUCLID:56
.=
p
by A60, A67, EUCLID:53
;
hence
a2 in LSeg (
|[b,c]|,
|[b,d]|)
by A59, A64, A65, A66;
verum end; case
d = c
;
a2 in LSeg (|[b,c]|,|[b,d]|)then A68:
p `2 = c
by A61, A62, XXREAL_0:1;
reconsider lambda =
0 as
Real ;
((1 - lambda) * |[b,c]|) + (lambda * |[b,d]|) =
|[((1 - lambda) * b),((1 - lambda) * c)]| + (lambda * |[b,d]|)
by EUCLID:58
.=
|[((1 - lambda) * b),((1 - lambda) * c)]| + |[(lambda * b),(lambda * d)]|
by EUCLID:58
.=
|[(((1 - lambda) * b) + (lambda * b)),(((1 - lambda) * c) + (lambda * d))]|
by EUCLID:56
.=
p
by A60, A68, EUCLID:53
;
hence
a2 in LSeg (
|[b,c]|,
|[b,d]|)
by A59;
verum end;
hence
a2 in LSeg (
|[b,c]|,
|[b,d]|)
;
verum
end;
LSeg (|[b,c]|,|[b,d]|) c= { p where p is Point of (TOP-REAL 2) : ( p `1 = b & p `2 <= d & p `2 >= c ) }
proof
let a2 be
object ;
TARSKI:def 3 ( not a2 in LSeg (|[b,c]|,|[b,d]|) or a2 in { p where p is Point of (TOP-REAL 2) : ( p `1 = b & p `2 <= d & p `2 >= c ) } )
assume
a2 in LSeg (
|[b,c]|,
|[b,d]|)
;
a2 in { p where p is Point of (TOP-REAL 2) : ( p `1 = b & p `2 <= d & p `2 >= c ) }
then consider lambda being
Real such that A69:
a2 = ((1 - lambda) * |[b,c]|) + (lambda * |[b,d]|)
and A70:
0 <= lambda
and A71:
lambda <= 1
;
set q =
((1 - lambda) * |[b,c]|) + (lambda * |[b,d]|);
A72:
(((1 - lambda) * |[b,c]|) + (lambda * |[b,d]|)) `1 =
(((1 - lambda) * |[b,c]|) `1) + ((lambda * |[b,d]|) `1)
by TOPREAL3:2
.=
((1 - lambda) * (|[b,c]| `1)) + ((lambda * |[b,d]|) `1)
by TOPREAL3:4
.=
((1 - lambda) * (|[b,c]| `1)) + (lambda * (|[b,d]| `1))
by TOPREAL3:4
.=
((1 - lambda) * b) + (lambda * b)
by A5, EUCLID:52
.=
b
;
A73:
(((1 - lambda) * |[b,c]|) + (lambda * |[b,d]|)) `2 =
(((1 - lambda) * |[b,c]|) `2) + ((lambda * |[b,d]|) `2)
by TOPREAL3:2
.=
((1 - lambda) * (|[b,c]| `2)) + ((lambda * |[b,d]|) `2)
by TOPREAL3:4
.=
((1 - lambda) * (|[b,c]| `2)) + (lambda * (|[b,d]| `2))
by TOPREAL3:4
.=
((1 - lambda) * c) + (lambda * d)
by A6, EUCLID:52
;
then A74:
(((1 - lambda) * |[b,c]|) + (lambda * |[b,d]|)) `2 <= d
by A2, A71, XREAL_1:172;
(((1 - lambda) * |[b,c]|) + (lambda * |[b,d]|)) `2 >= c
by A2, A70, A71, A73, XREAL_1:173;
hence
a2 in { p where p is Point of (TOP-REAL 2) : ( p `1 = b & p `2 <= d & p `2 >= c ) }
by A69, A72, A74;
verum
end;
hence
{ p where p is Point of (TOP-REAL 2) : ( p `1 = b & p `2 <= d & p `2 >= c ) } = LSeg (|[b,c]|,|[b,d]|)
by A58; verum