let a, b, c, d be real number ; :: thesis: ( 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 A1:
( a <= b & c <= d )
; :: thesis: ( 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]|;
A2:
( |[a,d]| `1 = a & |[a,d]| `2 = d )
by EUCLID:56;
A3:
( |[b,c]| `1 = b & |[b,c]| `2 = c )
by EUCLID:56;
thus
{ p where p is Point of (TOP-REAL 2) : ( p `1 = a & p `2 <= d & p `2 >= c ) } = LSeg |[a,c]|,|[a,d]|
:: thesis: ( 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 ) } )proof
A4:
{ 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
set ;
:: according to TARSKI:def 3 :: thesis: ( 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 ) }
;
:: thesis: a2 in LSeg |[a,c]|,|[a,d]|
then consider p being
Point of
(TOP-REAL 2) such that A5:
a2 = p
and A6:
(
p `1 = a &
p `2 <= d &
p `2 >= c )
;
now per cases
( d <> c or d = c )
;
case A7:
d <> c
;
:: thesis: a2 in LSeg |[a,c]|,|[a,d]|reconsider lambda =
((p `2 ) - c) / (d - c) as
Real ;
d >= c
by A6, XXREAL_0:2;
then
d > c
by A7, XXREAL_0:1;
then A8:
d - c > 0
by XREAL_1:52;
(p `2 ) - c >= 0
by A6, XREAL_1:50;
then A9:
lambda >= 0
by A8;
d - c >= (p `2 ) - c
by A6, XREAL_1:11;
then
(d - c) / (d - c) >= ((p `2 ) - c) / (d - c)
by A8, XREAL_1:74;
then A10:
1
>= lambda
by A8, XCMPLX_1:60;
A11:
((1 - lambda) * c) + (lambda * d) =
((((d - c) / (d - c)) - (((p `2 ) - c) / (d - c))) * c) + ((((p `2 ) - c) / (d - c)) * d)
by A8, XCMPLX_1:60
.=
((((d - c) - ((p `2 ) - c)) / (d - c)) * c) + ((((p `2 ) - c) / (d - c)) * d)
by XCMPLX_1:121
.=
(c * ((d - (p `2 )) / (d - c))) + ((d * ((p `2 ) - c)) / (d - c))
by XCMPLX_1:75
.=
((c * (d - (p `2 ))) / (d - c)) + ((d * ((p `2 ) - c)) / (d - c))
by XCMPLX_1:75
.=
(((c * d) - (c * (p `2 ))) + ((d * (p `2 )) - (d * c))) / (d - c)
by XCMPLX_1:63
.=
((d - c) * (p `2 )) / (d - c)
.=
(p `2 ) * ((d - c) / (d - c))
by XCMPLX_1:75
.=
(p `2 ) * 1
by A8, XCMPLX_1:60
.=
p `2
;
((1 - lambda) * |[a,c]|) + (lambda * |[a,d]|) =
|[((1 - lambda) * a),((1 - lambda) * c)]| + (lambda * |[a,d]|)
by EUCLID:62
.=
|[((1 - lambda) * a),((1 - lambda) * c)]| + |[(lambda * a),(lambda * d)]|
by EUCLID:62
.=
|[(((1 - lambda) * a) + (lambda * a)),(((1 - lambda) * c) + (lambda * d))]|
by EUCLID:60
.=
p
by A6, A11, EUCLID:57
;
hence
a2 in LSeg |[a,c]|,
|[a,d]|
by A5, A9, A10;
:: thesis: verum end; case
d = c
;
:: thesis: a2 in LSeg |[a,c]|,|[a,d]|then A12:
p `2 = c
by A6, 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:62
.=
|[((1 - lambda) * a),((1 - lambda) * c)]| + |[(lambda * a),(lambda * d)]|
by EUCLID:62
.=
|[(((1 - lambda) * a) + (lambda * a)),(((1 - lambda) * c) + (lambda * d))]|
by EUCLID:60
.=
p
by A6, A12, EUCLID:57
;
hence
a2 in LSeg |[a,c]|,
|[a,d]|
by A5;
:: thesis: verum end;
hence
a2 in LSeg |[a,c]|,
|[a,d]|
;
:: thesis: 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
set ;
:: according to TARSKI:def 3 :: thesis: ( 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]|
;
:: thesis: 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 A13:
(
a2 = ((1 - lambda) * |[a,c]|) + (lambda * |[a,d]|) &
0 <= lambda &
lambda <= 1 )
;
set q =
((1 - lambda) * |[a,c]|) + (lambda * |[a,d]|);
A14:
(((1 - lambda) * |[a,c]|) + (lambda * |[a,d]|)) `1 =
(((1 - lambda) * |[a,c]|) `1 ) + ((lambda * |[a,d]|) `1 )
by TOPREAL3:7
.=
((1 - lambda) * (|[a,c]| `1 )) + ((lambda * |[a,d]|) `1 )
by TOPREAL3:9
.=
((1 - lambda) * (|[a,c]| `1 )) + (lambda * (|[a,d]| `1 ))
by TOPREAL3:9
.=
((1 - lambda) * a) + (lambda * a)
by A2, EUCLID:56
.=
a
;
(((1 - lambda) * |[a,c]|) + (lambda * |[a,d]|)) `2 =
(((1 - lambda) * |[a,c]|) `2 ) + ((lambda * |[a,d]|) `2 )
by TOPREAL3:7
.=
((1 - lambda) * (|[a,c]| `2 )) + ((lambda * |[a,d]|) `2 )
by TOPREAL3:9
.=
((1 - lambda) * (|[a,c]| `2 )) + (lambda * (|[a,d]| `2 ))
by TOPREAL3:9
.=
((1 - lambda) * c) + (lambda * d)
by A2, EUCLID:56
;
then
(
(((1 - lambda) * |[a,c]|) + (lambda * |[a,d]|)) `1 = a &
(((1 - lambda) * |[a,c]|) + (lambda * |[a,d]|)) `2 <= d &
(((1 - lambda) * |[a,c]|) + (lambda * |[a,d]|)) `2 >= c )
by A1, A13, A14, XREAL_1:174, XREAL_1:175;
hence
a2 in { p where p is Point of (TOP-REAL 2) : ( p `1 = a & p `2 <= d & p `2 >= c ) }
by A13;
:: thesis: 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 A4, XBOOLE_0:def 10;
:: thesis: verum
end;
thus
{ p where p is Point of (TOP-REAL 2) : ( p `1 <= b & p `1 >= a & p `2 = d ) } = LSeg |[a,d]|,|[b,d]|
:: thesis: ( 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 ) } )proof
A15:
{ 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
set ;
:: according to TARSKI:def 3 :: thesis: ( 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 ) }
;
:: thesis: a2 in LSeg |[a,d]|,|[b,d]|
then consider p being
Point of
(TOP-REAL 2) such that A16:
a2 = p
and A17:
(
p `1 <= b &
p `1 >= a &
p `2 = d )
;
now per cases
( b <> a or b = a )
;
case A18:
b <> a
;
:: thesis: a2 in LSeg |[a,d]|,|[b,d]|reconsider lambda =
((p `1 ) - a) / (b - a) as
Real ;
b >= a
by A17, XXREAL_0:2;
then
b > a
by A18, XXREAL_0:1;
then A19:
b - a > 0
by XREAL_1:52;
(p `1 ) - a >= 0
by A17, XREAL_1:50;
then A20:
lambda >= 0
by A19;
b - a >= (p `1 ) - a
by A17, XREAL_1:11;
then
(b - a) / (b - a) >= ((p `1 ) - a) / (b - a)
by A19, XREAL_1:74;
then A21:
1
>= lambda
by A19, XCMPLX_1:60;
A22:
((1 - lambda) * a) + (lambda * b) =
((((b - a) / (b - a)) - (((p `1 ) - a) / (b - a))) * a) + ((((p `1 ) - a) / (b - a)) * b)
by A19, XCMPLX_1:60
.=
((((b - a) - ((p `1 ) - a)) / (b - a)) * a) + ((((p `1 ) - a) / (b - a)) * b)
by XCMPLX_1:121
.=
(a * ((b - (p `1 )) / (b - a))) + ((b * ((p `1 ) - a)) / (b - a))
by XCMPLX_1:75
.=
((a * (b - (p `1 ))) / (b - a)) + ((b * ((p `1 ) - a)) / (b - a))
by XCMPLX_1:75
.=
(((a * b) - (a * (p `1 ))) + ((b * (p `1 )) - (b * a))) / (b - a)
by XCMPLX_1:63
.=
((b - a) * (p `1 )) / (b - a)
.=
(p `1 ) * ((b - a) / (b - a))
by XCMPLX_1:75
.=
(p `1 ) * 1
by A19, XCMPLX_1:60
.=
p `1
;
((1 - lambda) * |[a,d]|) + (lambda * |[b,d]|) =
|[((1 - lambda) * a),((1 - lambda) * d)]| + (lambda * |[b,d]|)
by EUCLID:62
.=
|[((1 - lambda) * a),((1 - lambda) * d)]| + |[(lambda * b),(lambda * d)]|
by EUCLID:62
.=
|[(((1 - lambda) * a) + (lambda * b)),(((1 - lambda) * d) + (lambda * d))]|
by EUCLID:60
.=
p
by A17, A22, EUCLID:57
;
hence
a2 in LSeg |[a,d]|,
|[b,d]|
by A16, A20, A21;
:: thesis: verum end; case
b = a
;
:: thesis: a2 in LSeg |[a,d]|,|[b,d]|then A23:
p `1 = a
by A17, 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:62
.=
|[((1 - lambda) * a),((1 - lambda) * d)]| + |[(lambda * b),(lambda * d)]|
by EUCLID:62
.=
|[(((1 - lambda) * a) + (lambda * b)),(((1 - lambda) * d) + (lambda * d))]|
by EUCLID:60
.=
p
by A17, A23, EUCLID:57
;
hence
a2 in LSeg |[a,d]|,
|[b,d]|
by A16;
:: thesis: verum end;
hence
a2 in LSeg |[a,d]|,
|[b,d]|
;
:: thesis: 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
set ;
:: according to TARSKI:def 3 :: thesis: ( 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]|
;
:: thesis: 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 A24:
(
a2 = ((1 - lambda) * |[a,d]|) + (lambda * |[b,d]|) &
0 <= lambda &
lambda <= 1 )
;
set q =
((1 - lambda) * |[a,d]|) + (lambda * |[b,d]|);
A25:
(((1 - lambda) * |[a,d]|) + (lambda * |[b,d]|)) `2 =
(((1 - lambda) * |[a,d]|) `2 ) + ((lambda * |[b,d]|) `2 )
by TOPREAL3:7
.=
((1 - lambda) * (|[a,d]| `2 )) + ((lambda * |[b,d]|) `2 )
by TOPREAL3:9
.=
((1 - lambda) * (|[a,d]| `2 )) + (lambda * (|[b,d]| `2 ))
by TOPREAL3:9
.=
((1 - lambda) * d) + (lambda * d)
by A2, EUCLID:56
.=
d
;
(((1 - lambda) * |[a,d]|) + (lambda * |[b,d]|)) `1 =
(((1 - lambda) * |[a,d]|) `1 ) + ((lambda * |[b,d]|) `1 )
by TOPREAL3:7
.=
((1 - lambda) * (|[a,d]| `1 )) + ((lambda * |[b,d]|) `1 )
by TOPREAL3:9
.=
((1 - lambda) * (|[a,d]| `1 )) + (lambda * (|[b,d]| `1 ))
by TOPREAL3:9
.=
((1 - lambda) * a) + (lambda * b)
by A2, EUCLID:56
;
then
(
(((1 - lambda) * |[a,d]|) + (lambda * |[b,d]|)) `2 = d &
(((1 - lambda) * |[a,d]|) + (lambda * |[b,d]|)) `1 <= b &
(((1 - lambda) * |[a,d]|) + (lambda * |[b,d]|)) `1 >= a )
by A1, A24, A25, XREAL_1:174, XREAL_1:175;
hence
a2 in { p where p is Point of (TOP-REAL 2) : ( p `1 <= b & p `1 >= a & p `2 = d ) }
by A24;
:: thesis: 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 A15, XBOOLE_0:def 10;
:: thesis: verum
end;
thus
{ p where p is Point of (TOP-REAL 2) : ( p `1 <= b & p `1 >= a & p `2 = c ) } = LSeg |[a,c]|,|[b,c]|
:: thesis: LSeg |[b,c]|,|[b,d]| = { q2 where q2 is Point of (TOP-REAL 2) : ( q2 `1 = b & q2 `2 <= d & q2 `2 >= c ) } proof
A26:
{ 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
set ;
:: according to TARSKI:def 3 :: thesis: ( 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 ) }
;
:: thesis: a2 in LSeg |[a,c]|,|[b,c]|
then consider p being
Point of
(TOP-REAL 2) such that A27:
a2 = p
and A28:
(
p `1 <= b &
p `1 >= a &
p `2 = c )
;
now per cases
( b <> a or b = a )
;
case A29:
b <> a
;
:: thesis: a2 in LSeg |[a,c]|,|[b,c]|reconsider lambda =
((p `1 ) - a) / (b - a) as
Real ;
b >= a
by A28, XXREAL_0:2;
then
b > a
by A29, XXREAL_0:1;
then A30:
b - a > 0
by XREAL_1:52;
(p `1 ) - a >= 0
by A28, XREAL_1:50;
then A31:
lambda >= 0
by A30;
b - a >= (p `1 ) - a
by A28, XREAL_1:11;
then
(b - a) / (b - a) >= ((p `1 ) - a) / (b - a)
by A30, XREAL_1:74;
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:121
.=
(a * ((b - (p `1 )) / (b - a))) + ((b * ((p `1 ) - a)) / (b - a))
by XCMPLX_1:75
.=
((a * (b - (p `1 ))) / (b - a)) + ((b * ((p `1 ) - a)) / (b - a))
by XCMPLX_1:75
.=
(((a * b) - (a * (p `1 ))) + ((b * (p `1 )) - (b * a))) / (b - a)
by XCMPLX_1:63
.=
((b - a) * (p `1 )) / (b - a)
.=
(p `1 ) * ((b - a) / (b - a))
by XCMPLX_1:75
.=
(p `1 ) * 1
by A30, XCMPLX_1:60
.=
p `1
;
((1 - lambda) * |[a,c]|) + (lambda * |[b,c]|) =
|[((1 - lambda) * a),((1 - lambda) * c)]| + (lambda * |[b,c]|)
by EUCLID:62
.=
|[((1 - lambda) * a),((1 - lambda) * c)]| + |[(lambda * b),(lambda * c)]|
by EUCLID:62
.=
|[(((1 - lambda) * a) + (lambda * b)),(((1 - lambda) * c) + (lambda * c))]|
by EUCLID:60
.=
p
by A28, A33, EUCLID:57
;
hence
a2 in LSeg |[a,c]|,
|[b,c]|
by A27, A31, A32;
:: thesis: verum end; case
b = a
;
:: thesis: a2 in LSeg |[a,c]|,|[b,c]|then A34:
p `1 = a
by A28, 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:62
.=
|[((1 - lambda) * a),((1 - lambda) * c)]| + |[(lambda * b),(lambda * c)]|
by EUCLID:62
.=
|[(((1 - lambda) * a) + (lambda * b)),(((1 - lambda) * c) + (lambda * c))]|
by EUCLID:60
.=
p
by A28, A34, EUCLID:57
;
hence
a2 in LSeg |[a,c]|,
|[b,c]|
by A27;
:: thesis: verum end;
hence
a2 in LSeg |[a,c]|,
|[b,c]|
;
:: thesis: 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
set ;
:: according to TARSKI:def 3 :: thesis: ( 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]|
;
:: thesis: 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 A35:
(
a2 = ((1 - lambda) * |[a,c]|) + (lambda * |[b,c]|) &
0 <= lambda &
lambda <= 1 )
;
set q =
((1 - lambda) * |[a,c]|) + (lambda * |[b,c]|);
A36:
(((1 - lambda) * |[a,c]|) + (lambda * |[b,c]|)) `2 =
(((1 - lambda) * |[a,c]|) `2 ) + ((lambda * |[b,c]|) `2 )
by TOPREAL3:7
.=
((1 - lambda) * (|[a,c]| `2 )) + ((lambda * |[b,c]|) `2 )
by TOPREAL3:9
.=
((1 - lambda) * (|[a,c]| `2 )) + (lambda * (|[b,c]| `2 ))
by TOPREAL3:9
.=
((1 - lambda) * c) + (lambda * c)
by A3, EUCLID:56
.=
c
;
(((1 - lambda) * |[a,c]|) + (lambda * |[b,c]|)) `1 =
(((1 - lambda) * |[a,c]|) `1 ) + ((lambda * |[b,c]|) `1 )
by TOPREAL3:7
.=
((1 - lambda) * (|[a,c]| `1 )) + ((lambda * |[b,c]|) `1 )
by TOPREAL3:9
.=
((1 - lambda) * (|[a,c]| `1 )) + (lambda * (|[b,c]| `1 ))
by TOPREAL3:9
.=
((1 - lambda) * a) + (lambda * b)
by A3, EUCLID:56
;
then
(
(((1 - lambda) * |[a,c]|) + (lambda * |[b,c]|)) `2 = c &
(((1 - lambda) * |[a,c]|) + (lambda * |[b,c]|)) `1 <= b &
(((1 - lambda) * |[a,c]|) + (lambda * |[b,c]|)) `1 >= a )
by A1, A35, A36, XREAL_1:174, XREAL_1:175;
hence
a2 in { p where p is Point of (TOP-REAL 2) : ( p `1 <= b & p `1 >= a & p `2 = c ) }
by A35;
:: thesis: 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 A26, XBOOLE_0:def 10;
:: thesis: verum
end;
thus
{ p where p is Point of (TOP-REAL 2) : ( p `1 = b & p `2 <= d & p `2 >= c ) } = LSeg |[b,c]|,|[b,d]|
:: thesis: verumproof
A37:
{ 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
set ;
:: according to TARSKI:def 3 :: thesis: ( 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 ) }
;
:: thesis: a2 in LSeg |[b,c]|,|[b,d]|
then consider p being
Point of
(TOP-REAL 2) such that A38:
a2 = p
and A39:
(
p `1 = b &
p `2 <= d &
p `2 >= c )
;
now per cases
( d <> c or d = c )
;
case A40:
d <> c
;
:: thesis: a2 in LSeg |[b,c]|,|[b,d]|reconsider lambda =
((p `2 ) - c) / (d - c) as
Real ;
d >= c
by A39, XXREAL_0:2;
then
d > c
by A40, XXREAL_0:1;
then A41:
d - c > 0
by XREAL_1:52;
(p `2 ) - c >= 0
by A39, XREAL_1:50;
then A42:
lambda >= 0
by A41;
d - c >= (p `2 ) - c
by A39, XREAL_1:11;
then
(d - c) / (d - c) >= ((p `2 ) - c) / (d - c)
by A41, XREAL_1:74;
then A43:
1
>= lambda
by A41, XCMPLX_1:60;
A44:
((1 - lambda) * c) + (lambda * d) =
((((d - c) / (d - c)) - (((p `2 ) - c) / (d - c))) * c) + ((((p `2 ) - c) / (d - c)) * d)
by A41, XCMPLX_1:60
.=
((((d - c) - ((p `2 ) - c)) / (d - c)) * c) + ((((p `2 ) - c) / (d - c)) * d)
by XCMPLX_1:121
.=
(c * ((d - (p `2 )) / (d - c))) + ((d * ((p `2 ) - c)) / (d - c))
by XCMPLX_1:75
.=
((c * (d - (p `2 ))) / (d - c)) + ((d * ((p `2 ) - c)) / (d - c))
by XCMPLX_1:75
.=
(((c * d) - (c * (p `2 ))) + ((d * (p `2 )) - (d * c))) / (d - c)
by XCMPLX_1:63
.=
((d - c) * (p `2 )) / (d - c)
.=
(p `2 ) * ((d - c) / (d - c))
by XCMPLX_1:75
.=
(p `2 ) * 1
by A41, XCMPLX_1:60
.=
p `2
;
((1 - lambda) * |[b,c]|) + (lambda * |[b,d]|) =
|[((1 - lambda) * b),((1 - lambda) * c)]| + (lambda * |[b,d]|)
by EUCLID:62
.=
|[((1 - lambda) * b),((1 - lambda) * c)]| + |[(lambda * b),(lambda * d)]|
by EUCLID:62
.=
|[(((1 - lambda) * b) + (lambda * b)),(((1 - lambda) * c) + (lambda * d))]|
by EUCLID:60
.=
p
by A39, A44, EUCLID:57
;
hence
a2 in LSeg |[b,c]|,
|[b,d]|
by A38, A42, A43;
:: thesis: verum end; case
d = c
;
:: thesis: a2 in LSeg |[b,c]|,|[b,d]|then A45:
p `2 = c
by A39, 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:62
.=
|[((1 - lambda) * b),((1 - lambda) * c)]| + |[(lambda * b),(lambda * d)]|
by EUCLID:62
.=
|[(((1 - lambda) * b) + (lambda * b)),(((1 - lambda) * c) + (lambda * d))]|
by EUCLID:60
.=
p
by A39, A45, EUCLID:57
;
hence
a2 in LSeg |[b,c]|,
|[b,d]|
by A38;
:: thesis: verum end;
hence
a2 in LSeg |[b,c]|,
|[b,d]|
;
:: thesis: 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
set ;
:: according to TARSKI:def 3 :: thesis: ( 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]|
;
:: thesis: 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 A46:
(
a2 = ((1 - lambda) * |[b,c]|) + (lambda * |[b,d]|) &
0 <= lambda &
lambda <= 1 )
;
set q =
((1 - lambda) * |[b,c]|) + (lambda * |[b,d]|);
A47:
(((1 - lambda) * |[b,c]|) + (lambda * |[b,d]|)) `1 =
(((1 - lambda) * |[b,c]|) `1 ) + ((lambda * |[b,d]|) `1 )
by TOPREAL3:7
.=
((1 - lambda) * (|[b,c]| `1 )) + ((lambda * |[b,d]|) `1 )
by TOPREAL3:9
.=
((1 - lambda) * (|[b,c]| `1 )) + (lambda * (|[b,d]| `1 ))
by TOPREAL3:9
.=
((1 - lambda) * b) + (lambda * b)
by A3, EUCLID:56
.=
b
;
(((1 - lambda) * |[b,c]|) + (lambda * |[b,d]|)) `2 =
(((1 - lambda) * |[b,c]|) `2 ) + ((lambda * |[b,d]|) `2 )
by TOPREAL3:7
.=
((1 - lambda) * (|[b,c]| `2 )) + ((lambda * |[b,d]|) `2 )
by TOPREAL3:9
.=
((1 - lambda) * (|[b,c]| `2 )) + (lambda * (|[b,d]| `2 ))
by TOPREAL3:9
.=
((1 - lambda) * c) + (lambda * d)
by A3, EUCLID:56
;
then
(
(((1 - lambda) * |[b,c]|) + (lambda * |[b,d]|)) `1 = b &
(((1 - lambda) * |[b,c]|) + (lambda * |[b,d]|)) `2 <= d &
(((1 - lambda) * |[b,c]|) + (lambda * |[b,d]|)) `2 >= c )
by A1, A46, A47, XREAL_1:174, XREAL_1:175;
hence
a2 in { p where p is Point of (TOP-REAL 2) : ( p `1 = b & p `2 <= d & p `2 >= c ) }
by A46;
:: thesis: 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 A37, XBOOLE_0:def 10;
:: thesis: verum
end;