let r, r1, s1 be Real; :: thesis: ( r1 <= s1 implies { p1 where p1 is Point of (TOP-REAL 2) : ( p1 `2 = r & r1 <= p1 `1 & p1 `1 <= s1 ) } = LSeg (|[r1,r]|,|[s1,r]|) )
set L = { p3 where p3 is Point of (TOP-REAL 2) : ( p3 `2 = r & r1 <= p3 `1 & p3 `1 <= s1 ) } ;
set p = |[r1,r]|;
set q = |[s1,r]|;
assume A2: r1 <= s1 ; :: thesis: { p1 where p1 is Point of (TOP-REAL 2) : ( p1 `2 = r & r1 <= p1 `1 & p1 `1 <= s1 ) } = LSeg (|[r1,r]|,|[s1,r]|)
then A3: s1 - r1 >= r1 - r1 by XREAL_1:13;
A4: |[s1,r]| `2 = r ;
A5: |[r1,r]| `2 = r ;
A6: |[s1,r]| `1 = s1 ;
thus { p3 where p3 is Point of (TOP-REAL 2) : ( p3 `2 = r & r1 <= p3 `1 & p3 `1 <= s1 ) } c= LSeg (|[r1,r]|,|[s1,r]|) :: according to XBOOLE_0:def 10 :: thesis: LSeg (|[r1,r]|,|[s1,r]|) c= { p1 where p1 is Point of (TOP-REAL 2) : ( p1 `2 = r & r1 <= p1 `1 & p1 `1 <= s1 ) }

proof

per cases ( r1 = s1 or r1 < s1 ) by A2, XXREAL_0:1;

suppose A7: r1 = s1 ; :: thesis: { p3 where p3 is Point of (TOP-REAL 2) : ( p3 `2 = r & r1 <= p3 `1 & p3 `1 <= s1 ) } c= LSeg (|[r1,r]|,|[s1,r]|)

{ p3 where p3 is Point of (TOP-REAL 2) : ( p3 `2 = r & r1 <= p3 `1 & p3 `1 <= s1 ) } c= {|[r1,r]|}

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { p3 where p3 is Point of (TOP-REAL 2) : ( p3 `2 = r & r1 <= p3 `1 & p3 `1 <= s1 ) } or x in {|[r1,r]|} )
assume x in { p3 where p3 is Point of (TOP-REAL 2) : ( p3 `2 = r & r1 <= p3 `1 & p3 `1 <= s1 ) } ; :: thesis: x in {|[r1,r]|}
then consider p2 being Point of (TOP-REAL 2) such that
A8: x = p2 and
A9: p2 `2 = r and
A10: ( r1 <= p2 `1 & p2 `1 <= s1 ) ;
|[r1,r]| `1 = p2 `1 by A7, A10, XXREAL_0:1;
then p2 = |[r1,r]| by A5, A9, Th6;
hence x in {|[r1,r]|} by A8, TARSKI:def 1; :: thesis: verum

end;

hence { p3 where p3 is Point of (TOP-REAL 2) : ( p3 `2 = r & r1 <= p3 `1 & p3 `1 <= s1 ) } c= LSeg (|[r1,r]|,|[s1,r]|) by A7, RLTOPSP1:70; :: thesis: verum

end;

suppose A11: r1 < s1 ; :: thesis: { p3 where p3 is Point of (TOP-REAL 2) : ( p3 `2 = r & r1 <= p3 `1 & p3 `1 <= s1 ) } c= LSeg (|[r1,r]|,|[s1,r]|)

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { p3 where p3 is Point of (TOP-REAL 2) : ( p3 `2 = r & r1 <= p3 `1 & p3 `1 <= s1 ) } or x in LSeg (|[r1,r]|,|[s1,r]|) )
assume x in { p3 where p3 is Point of (TOP-REAL 2) : ( p3 `2 = r & r1 <= p3 `1 & p3 `1 <= s1 ) } ; :: thesis: x in LSeg (|[r1,r]|,|[s1,r]|)
then consider p2 being Point of (TOP-REAL 2) such that
A12: x = p2 and
A13: p2 `2 = r and
A14: r1 <= p2 `1 and
A15: p2 `1 <= s1 ;
set t = p2 `1 ;
set l = ((p2 `1) - r1) / (s1 - r1);
A16: s1 - r1 > 0 by A11, XREAL_1:50;
then A17: 1 - (((p2 `1) - r1) / (s1 - r1)) = ((1 * (s1 - r1)) - ((p2 `1) - r1)) / (s1 - r1) by XCMPLX_1:127
.= (s1 - (p2 `1)) / (s1 - r1) ;
(p2 `1) - r1 <= s1 - r1 by A15, XREAL_1:9;
then ((p2 `1) - r1) / (s1 - r1) <= (s1 - r1) / (s1 - r1) by A16, XREAL_1:72;
then A18: ((p2 `1) - r1) / (s1 - r1) <= 1 by A16, XCMPLX_1:60;
A19: (((1 - (((p2 `1) - r1) / (s1 - r1))) * |[r1,r]|) + ((((p2 `1) - r1) / (s1 - r1)) * |[s1,r]|)) `2 = (((1 - (((p2 `1) - r1) / (s1 - r1))) * |[r1,r]|) `2) + (((((p2 `1) - r1) / (s1 - r1)) * |[s1,r]|) `2) by Th2
.= ((1 - (((p2 `1) - r1) / (s1 - r1))) * (|[r1,r]| `2)) + (((((p2 `1) - r1) / (s1 - r1)) * |[s1,r]|) `2) by Th4
.= ((1 - (((p2 `1) - r1) / (s1 - r1))) * r) + ((((p2 `1) - r1) / (s1 - r1)) * r) by A4, Th4
.= p2 `2 by A13 ;
(((1 - (((p2 `1) - r1) / (s1 - r1))) * |[r1,r]|) + ((((p2 `1) - r1) / (s1 - r1)) * |[s1,r]|)) `1 = (((1 - (((p2 `1) - r1) / (s1 - r1))) * |[r1,r]|) `1) + (((((p2 `1) - r1) / (s1 - r1)) * |[s1,r]|) `1) by Th2
.= ((1 - (((p2 `1) - r1) / (s1 - r1))) * (|[r1,r]| `1)) + (((((p2 `1) - r1) / (s1 - r1)) * |[s1,r]|) `1) by Th4
.= ((1 - (((p2 `1) - r1) / (s1 - r1))) * (|[r1,r]| `1)) + ((((p2 `1) - r1) / (s1 - r1)) * (|[s1,r]| `1)) by Th4
.= (((s1 - (p2 `1)) * (|[r1,r]| `1)) / (s1 - r1)) + ((((p2 `1) - r1) / (s1 - r1)) * (|[s1,r]| `1)) by A17, XCMPLX_1:74
.= (((s1 - (p2 `1)) * (|[r1,r]| `1)) / (s1 - r1)) + ((((p2 `1) - r1) * (|[s1,r]| `1)) / (s1 - r1)) by XCMPLX_1:74
.= (((s1 * r1) - ((p2 `1) * r1)) + (((p2 `1) - r1) * s1)) / (s1 - r1) by XCMPLX_1:62
.= ((p2 `1) * (s1 - r1)) / (s1 - r1)
.= (p2 `1) * ((s1 - r1) / (s1 - r1)) by XCMPLX_1:74
.= (p2 `1) * 1 by A16, XCMPLX_1:60
.= p2 `1 ;
then A20: p2 = ((1 - (((p2 `1) - r1) / (s1 - r1))) * |[r1,r]|) + ((((p2 `1) - r1) / (s1 - r1)) * |[s1,r]|) by A19, Th6;
r1 - r1 <= (p2 `1) - r1 by A14, XREAL_1:9;
hence x in LSeg (|[r1,r]|,|[s1,r]|) by A16, A12, A18, A20; :: thesis: verum

end;

end;

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in LSeg (|[r1,r]|,|[s1,r]|) or x in { p1 where p1 is Point of (TOP-REAL 2) : ( p1 `2 = r & r1 <= p1 `1 & p1 `1 <= s1 ) } )
assume x in LSeg (|[r1,r]|,|[s1,r]|) ; :: thesis: x in { p1 where p1 is Point of (TOP-REAL 2) : ( p1 `2 = r & r1 <= p1 `1 & p1 `1 <= s1 ) }
then consider lambda being Real such that
A21: ((1 - lambda) * |[r1,r]|) + (lambda * |[s1,r]|) = x and
A22: 0 <= lambda and
A23: lambda <= 1 ;
A24: r1 + 0 <= r1 + (lambda * (s1 - r1)) by A3, A22, XREAL_1:7;
lambda * (s1 - r1) <= 1 * (s1 - r1) by A3, A23, XREAL_1:64;
then A25: r1 + (lambda * (s1 - r1)) <= (s1 - r1) + r1 by XREAL_1:7;
set p2 = ((1 - lambda) * |[r1,r]|) + (lambda * |[s1,r]|);
A26: (((1 - lambda) * |[r1,r]|) + (lambda * |[s1,r]|)) `1 = (((1 - lambda) * |[r1,r]|) `1) + ((lambda * |[s1,r]|) `1) by Th2
.= ((1 - lambda) * (|[r1,r]| `1)) + ((lambda * |[s1,r]|) `1) by Th4
.= ((1 * r1) - (lambda * r1)) + (lambda * s1) by A6, Th4
.= r1 + (lambda * (s1 - r1)) ;
(((1 - lambda) * |[r1,r]|) + (lambda * |[s1,r]|)) `2 = (((1 - lambda) * |[r1,r]|) `2) + ((lambda * |[s1,r]|) `2) by Th2
.= ((1 - lambda) * (|[r1,r]| `2)) + ((lambda * |[s1,r]|) `2) by Th4
.= ((1 - lambda) * r) + (lambda * r) by A4, Th4
.= r ;
hence x in { p1 where p1 is Point of (TOP-REAL 2) : ( p1 `2 = r & r1 <= p1 `1 & p1 `1 <= s1 ) } by A21, A26, A24, A25; :: thesis: verum