let a, b, c, d be Real; :: thesis: ( a <= b & c <= d implies ( LSeg (|[a,c]|,|[a,d]|) = { p1 where p1 is Point of () : ( p1 `1 = a & p1 `2 <= d & p1 `2 >= c ) } & LSeg (|[a,d]|,|[b,d]|) = { p2 where p2 is Point of () : ( p2 `1 <= b & p2 `1 >= a & p2 `2 = d ) } & LSeg (|[a,c]|,|[b,c]|) = { q1 where q1 is Point of () : ( q1 `1 <= b & q1 `1 >= a & q1 `2 = c ) } & LSeg (|[b,c]|,|[b,d]|) = { q2 where q2 is Point of () : ( q2 `1 = b & q2 `2 <= d & q2 `2 >= c ) } ) )
assume that
A1: a <= b and
A2: c <= d ; :: thesis: ( LSeg (|[a,c]|,|[a,d]|) = { p1 where p1 is Point of () : ( p1 `1 = a & p1 `2 <= d & p1 `2 >= c ) } & LSeg (|[a,d]|,|[b,d]|) = { p2 where p2 is Point of () : ( p2 `1 <= b & p2 `1 >= a & p2 `2 = d ) } & LSeg (|[a,c]|,|[b,c]|) = { q1 where q1 is Point of () : ( q1 `1 <= b & q1 `1 >= a & q1 `2 = c ) } & LSeg (|[b,c]|,|[b,d]|) = { q2 where q2 is Point of () : ( q2 `1 = b & q2 `2 <= d & q2 `2 >= c ) } )
set L1 = { p where p is Point of () : ( p `1 = a & p `2 <= d & p `2 >= c ) } ;
set L2 = { p where p is Point of () : ( p `1 <= b & p `1 >= a & p `2 = d ) } ;
set L3 = { p where p is Point of () : ( p `1 <= b & p `1 >= a & p `2 = c ) } ;
set L4 = { p where p is Point of () : ( 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 () : ( p `1 = a & p `2 <= d & p `2 >= c ) } c= LSeg (|[a,c]|,|[a,d]|)
proof
let a2 be object ; :: according to TARSKI:def 3 :: thesis: ( not a2 in { p where p is Point of () : ( 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 () : ( p `1 = a & p `2 <= d & p `2 >= c ) } ; :: thesis: a2 in LSeg (|[a,c]|,|[a,d]|)
then consider p being Point of () such that
A8: a2 = p and
A9: p `1 = a and
A10: p `2 <= d and
A11: p `2 >= c ;
now :: thesis: ( ( 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 ; :: thesis: a2 in LSeg (|[a,c]|,|[a,d]|)
reconsider lambda = ((p `2) - c) / (d - c) as Real ;
d >= c by ;
then d > c by ;
then A13: d - c > 0 by XREAL_1:50;
A14: (p `2) - c >= 0 by ;
d - c >= (p `2) - c by ;
then (d - c) / (d - c) >= ((p `2) - c) / (d - c) by ;
then A15: 1 >= lambda by ;
A16: ((1 - lambda) * c) + (lambda * d) = ((((d - c) / (d - c)) - (((p `2) - c) / (d - c))) * c) + ((((p `2) - c) / (d - c)) * d) by
.= ((((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
.= 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 ;
hence a2 in LSeg (|[a,c]|,|[a,d]|) by A8, A13, A14, A15; :: thesis: verum
end;
case d = c ; :: thesis: a2 in LSeg (|[a,c]|,|[a,d]|)
then A17: p `2 = c by ;
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 ;
hence a2 in LSeg (|[a,c]|,|[a,d]|) by A8; :: thesis: verum
end;
end;
end;
hence a2 in LSeg (|[a,c]|,|[a,d]|) ; :: thesis: verum
end;
LSeg (|[a,c]|,|[a,d]|) c= { p where p is Point of () : ( p `1 = a & p `2 <= d & p `2 >= c ) }
proof
let a2 be object ; :: according to TARSKI:def 3 :: thesis: ( not a2 in LSeg (|[a,c]|,|[a,d]|) or a2 in { p where p is Point of () : ( 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 () : ( 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
.= 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 ;
then A23: (((1 - lambda) * |[a,c]|) + (lambda * |[a,d]|)) `2 <= d by ;
(((1 - lambda) * |[a,c]|) + (lambda * |[a,d]|)) `2 >= c by ;
hence a2 in { p where p is Point of () : ( p `1 = a & p `2 <= d & p `2 >= c ) } by ; :: thesis: verum
end;
hence { p where p is Point of () : ( p `1 = a & p `2 <= d & p `2 >= c ) } = LSeg (|[a,c]|,|[a,d]|) by A7; :: thesis: ( LSeg (|[a,d]|,|[b,d]|) = { p2 where p2 is Point of () : ( p2 `1 <= b & p2 `1 >= a & p2 `2 = d ) } & LSeg (|[a,c]|,|[b,c]|) = { q1 where q1 is Point of () : ( q1 `1 <= b & q1 `1 >= a & q1 `2 = c ) } & LSeg (|[b,c]|,|[b,d]|) = { q2 where q2 is Point of () : ( q2 `1 = b & q2 `2 <= d & q2 `2 >= c ) } )
A24: { p where p is Point of () : ( p `1 <= b & p `1 >= a & p `2 = d ) } c= LSeg (|[a,d]|,|[b,d]|)
proof
let a2 be object ; :: according to TARSKI:def 3 :: thesis: ( not a2 in { p where p is Point of () : ( 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 () : ( p `1 <= b & p `1 >= a & p `2 = d ) } ; :: thesis: a2 in LSeg (|[a,d]|,|[b,d]|)
then consider p being Point of () such that
A25: a2 = p and
A26: p `1 <= b and
A27: p `1 >= a and
A28: p `2 = d ;
now :: thesis: ( ( 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 ; :: thesis: a2 in LSeg (|[a,d]|,|[b,d]|)
reconsider lambda = ((p `1) - a) / (b - a) as Real ;
b >= a by ;
then b > a by ;
then A30: b - a > 0 by XREAL_1:50;
A31: (p `1) - a >= 0 by ;
b - a >= (p `1) - a by ;
then (b - a) / (b - a) >= ((p `1) - a) / (b - a) by ;
then A32: 1 >= lambda by ;
A33: ((1 - lambda) * a) + (lambda * b) = ((((b - a) / (b - a)) - (((p `1) - a) / (b - a))) * a) + ((((p `1) - a) / (b - a)) * b) by
.= ((((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
.= 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 ;
hence a2 in LSeg (|[a,d]|,|[b,d]|) by A25, A30, A31, A32; :: thesis: verum
end;
case b = a ; :: thesis: a2 in LSeg (|[a,d]|,|[b,d]|)
then A34: p `1 = a by ;
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 ;
hence a2 in LSeg (|[a,d]|,|[b,d]|) by A25; :: thesis: verum
end;
end;
end;
hence a2 in LSeg (|[a,d]|,|[b,d]|) ; :: thesis: verum
end;
LSeg (|[a,d]|,|[b,d]|) c= { p where p is Point of () : ( p `1 <= b & p `1 >= a & p `2 = d ) }
proof
let a2 be object ; :: according to TARSKI:def 3 :: thesis: ( not a2 in LSeg (|[a,d]|,|[b,d]|) or a2 in { p where p is Point of () : ( 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 () : ( 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
.= 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 ;
then A40: (((1 - lambda) * |[a,d]|) + (lambda * |[b,d]|)) `1 <= b by ;
(((1 - lambda) * |[a,d]|) + (lambda * |[b,d]|)) `1 >= a by ;
hence a2 in { p where p is Point of () : ( p `1 <= b & p `1 >= a & p `2 = d ) } by ; :: thesis: verum
end;
hence { p where p is Point of () : ( p `1 <= b & p `1 >= a & p `2 = d ) } = LSeg (|[a,d]|,|[b,d]|) by A24; :: thesis: ( LSeg (|[a,c]|,|[b,c]|) = { q1 where q1 is Point of () : ( q1 `1 <= b & q1 `1 >= a & q1 `2 = c ) } & LSeg (|[b,c]|,|[b,d]|) = { q2 where q2 is Point of () : ( q2 `1 = b & q2 `2 <= d & q2 `2 >= c ) } )
A41: { p where p is Point of () : ( p `1 <= b & p `1 >= a & p `2 = c ) } c= LSeg (|[a,c]|,|[b,c]|)
proof
let a2 be object ; :: according to TARSKI:def 3 :: thesis: ( not a2 in { p where p is Point of () : ( 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 () : ( p `1 <= b & p `1 >= a & p `2 = c ) } ; :: thesis: a2 in LSeg (|[a,c]|,|[b,c]|)
then consider p being Point of () such that
A42: a2 = p and
A43: p `1 <= b and
A44: p `1 >= a and
A45: p `2 = c ;
now :: thesis: ( ( 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 ; :: thesis: a2 in LSeg (|[a,c]|,|[b,c]|)
reconsider lambda = ((p `1) - a) / (b - a) as Real ;
b >= a by ;
then b > a by ;
then A47: b - a > 0 by XREAL_1:50;
A48: (p `1) - a >= 0 by ;
b - a >= (p `1) - a by ;
then (b - a) / (b - a) >= ((p `1) - a) / (b - a) by ;
then A49: 1 >= lambda by ;
A50: ((1 - lambda) * a) + (lambda * b) = ((((b - a) / (b - a)) - (((p `1) - a) / (b - a))) * a) + ((((p `1) - a) / (b - a)) * b) by
.= ((((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
.= 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 ;
hence a2 in LSeg (|[a,c]|,|[b,c]|) by A42, A47, A48, A49; :: thesis: verum
end;
case b = a ; :: thesis: a2 in LSeg (|[a,c]|,|[b,c]|)
then A51: p `1 = a by ;
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 ;
hence a2 in LSeg (|[a,c]|,|[b,c]|) by A42; :: thesis: verum
end;
end;
end;
hence a2 in LSeg (|[a,c]|,|[b,c]|) ; :: thesis: verum
end;
LSeg (|[a,c]|,|[b,c]|) c= { p where p is Point of () : ( p `1 <= b & p `1 >= a & p `2 = c ) }
proof
let a2 be object ; :: according to TARSKI:def 3 :: thesis: ( not a2 in LSeg (|[a,c]|,|[b,c]|) or a2 in { p where p is Point of () : ( 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 () : ( 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
.= 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 ;
then A57: (((1 - lambda) * |[a,c]|) + (lambda * |[b,c]|)) `1 <= b by ;
(((1 - lambda) * |[a,c]|) + (lambda * |[b,c]|)) `1 >= a by ;
hence a2 in { p where p is Point of () : ( p `1 <= b & p `1 >= a & p `2 = c ) } by ; :: thesis: verum
end;
hence { p where p is Point of () : ( p `1 <= b & p `1 >= a & p `2 = c ) } = LSeg (|[a,c]|,|[b,c]|) by A41; :: thesis: LSeg (|[b,c]|,|[b,d]|) = { q2 where q2 is Point of () : ( q2 `1 = b & q2 `2 <= d & q2 `2 >= c ) }
A58: { p where p is Point of () : ( p `1 = b & p `2 <= d & p `2 >= c ) } c= LSeg (|[b,c]|,|[b,d]|)
proof
let a2 be object ; :: according to TARSKI:def 3 :: thesis: ( not a2 in { p where p is Point of () : ( 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 () : ( p `1 = b & p `2 <= d & p `2 >= c ) } ; :: thesis: a2 in LSeg (|[b,c]|,|[b,d]|)
then consider p being Point of () such that
A59: a2 = p and
A60: p `1 = b and
A61: p `2 <= d and
A62: p `2 >= c ;
now :: thesis: ( ( 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 ; :: thesis: a2 in LSeg (|[b,c]|,|[b,d]|)
reconsider lambda = ((p `2) - c) / (d - c) as Real ;
d >= c by ;
then d > c by ;
then A64: d - c > 0 by XREAL_1:50;
A65: (p `2) - c >= 0 by ;
d - c >= (p `2) - c by ;
then (d - c) / (d - c) >= ((p `2) - c) / (d - c) by ;
then A66: 1 >= lambda by ;
A67: ((1 - lambda) * c) + (lambda * d) = ((((d - c) / (d - c)) - (((p `2) - c) / (d - c))) * c) + ((((p `2) - c) / (d - c)) * d) by
.= ((((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
.= 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 ;
hence a2 in LSeg (|[b,c]|,|[b,d]|) by A59, A64, A65, A66; :: thesis: verum
end;
case d = c ; :: thesis: a2 in LSeg (|[b,c]|,|[b,d]|)
then A68: p `2 = c by ;
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 ;
hence a2 in LSeg (|[b,c]|,|[b,d]|) by A59; :: thesis: verum
end;
end;
end;
hence a2 in LSeg (|[b,c]|,|[b,d]|) ; :: thesis: verum
end;
LSeg (|[b,c]|,|[b,d]|) c= { p where p is Point of () : ( p `1 = b & p `2 <= d & p `2 >= c ) }
proof
let a2 be object ; :: according to TARSKI:def 3 :: thesis: ( not a2 in LSeg (|[b,c]|,|[b,d]|) or a2 in { p where p is Point of () : ( 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 () : ( 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
.= 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 ;
then A74: (((1 - lambda) * |[b,c]|) + (lambda * |[b,d]|)) `2 <= d by ;
(((1 - lambda) * |[b,c]|) + (lambda * |[b,d]|)) `2 >= c by ;
hence a2 in { p where p is Point of () : ( p `1 = b & p `2 <= d & p `2 >= c ) } by ; :: thesis: verum
end;
hence { p where p is Point of () : ( p `1 = b & p `2 <= d & p `2 >= c ) } = LSeg (|[b,c]|,|[b,d]|) by A58; :: thesis: verum