let a, b, c, d be Real; :: 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 that
A1: a <= b and
A2: 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]|;
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 ; :: 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
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 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; :: thesis: verum

end;

case d = c ; :: thesis: 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; :: 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 (TOP-REAL 2) : ( 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 (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
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; :: 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 A7; :: 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 ) } )
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 ; :: 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
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 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; :: thesis: verum

end;

case b = a ; :: thesis: 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; :: 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 (TOP-REAL 2) : ( 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 (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
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; :: 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 A24; :: 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 ) } )
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 ; :: 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
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 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; :: thesis: verum

end;

case b = a ; :: thesis: 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; :: 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 (TOP-REAL 2) : ( 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 (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
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; :: 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 A41; :: thesis: 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 ; :: 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
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 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; :: thesis: verum

end;

case d = c ; :: thesis: 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; :: 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 (TOP-REAL 2) : ( 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 (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
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; :: 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 A58; :: thesis: verum