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 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:56;
A4: |[a,d]| `2 = d by EUCLID:56;
A5: |[b,c]| `1 = b by EUCLID:56;
A6: |[b,c]| `2 = c by EUCLID:56;
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 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
A8: a2 = p and
A9: p `1 = a and
A10: p `2 <= d and
A11: p `2 >= c ;

now

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:52;
A14: (p `2 ) - c >= 0 by A11, XREAL_1:50;
d - c >= (p `2 ) - c by A10, XREAL_1:11;
then (d - c) / (d - c) >= ((p `2 ) - c) / (d - c) by A13, XREAL_1:74;
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: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 A13, 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 A9, A16, EUCLID:57 ;
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: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 A9, A17, EUCLID:57 ;
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 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
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: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 A3, EUCLID:56
.= a ;
A22: (((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 A4, EUCLID:56 ;
then A23: (((1 - lambda) * |[a,c]|) + (lambda * |[a,d]|)) `2 <= d by A2, A20, XREAL_1:174;
(((1 - lambda) * |[a,c]|) + (lambda * |[a,d]|)) `2 >= c by A2, A19, A20, A22, 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 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, XBOOLE_0:def 10; :: 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 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
A25: a2 = p and
A26: p `1 <= b and
A27: p `1 >= a and
A28: p `2 = d ;

now

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:52;
A31: (p `1 ) - a >= 0 by A27, XREAL_1:50;
b - a >= (p `1 ) - a by A26, 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,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 A28, A33, EUCLID:57 ;
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: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 A28, A34, EUCLID:57 ;
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 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
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: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 A4, EUCLID:56
.= d ;
A39: (((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 A3, EUCLID:56 ;
then A40: (((1 - lambda) * |[a,d]|) + (lambda * |[b,d]|)) `1 <= b by A1, A37, XREAL_1:174;
(((1 - lambda) * |[a,d]|) + (lambda * |[b,d]|)) `1 >= a by A1, A36, A37, A39, 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 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, XBOOLE_0:def 10; :: 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 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
A42: a2 = p and
A43: p `1 <= b and
A44: p `1 >= a and
A45: p `2 = c ;

now

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:52;
A48: (p `1 ) - a >= 0 by A44, XREAL_1:50;
b - a >= (p `1 ) - a by A43, XREAL_1:11;
then (b - a) / (b - a) >= ((p `1 ) - a) / (b - a) by A47, XREAL_1:74;
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: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 A47, 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 A45, A50, EUCLID:57 ;
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: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 A45, A51, EUCLID:57 ;
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 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
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: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 A6, EUCLID:56
.= c ;
A56: (((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 A5, EUCLID:56 ;
then A57: (((1 - lambda) * |[a,c]|) + (lambda * |[b,c]|)) `1 <= b by A1, A54, XREAL_1:174;
(((1 - lambda) * |[a,c]|) + (lambda * |[b,c]|)) `1 >= a by A1, A53, A54, A56, 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 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, XBOOLE_0:def 10; :: 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 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
A59: a2 = p and
A60: p `1 = b and
A61: p `2 <= d and
A62: p `2 >= c ;

now

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:52;
A65: (p `2 ) - c >= 0 by A62, XREAL_1:50;
d - c >= (p `2 ) - c by A61, XREAL_1:11;
then (d - c) / (d - c) >= ((p `2 ) - c) / (d - c) by A64, XREAL_1:74;
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: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 A64, 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 A60, A67, EUCLID:57 ;
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: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 A60, A68, EUCLID:57 ;
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 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
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: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 A5, EUCLID:56
.= b ;
A73: (((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 A6, EUCLID:56 ;
then A74: (((1 - lambda) * |[b,c]|) + (lambda * |[b,d]|)) `2 <= d by A2, A71, XREAL_1:174;
(((1 - lambda) * |[b,c]|) + (lambda * |[b,d]|)) `2 >= c by A2, A70, A71, A73, 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 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, XBOOLE_0:def 10; :: thesis: verum