let r1, s1, r be real number ; :: 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]| )
assume A1:
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 A2:
s1 - r1 >= r1 - r1
by XREAL_1:15;
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]|;
A3:
( |[r1,r]| `1 = r1 & |[r1,r]| `2 = r )
by EUCLID:56;
A4:
( |[s1,r]| `1 = s1 & |[s1,r]| `2 = r )
by EUCLID:56;
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 A1, XXREAL_0:1;
suppose A5:
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
set ;
:: 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 A6:
x = p2
and A7:
(
p2 `2 = r &
r1 <= p2 `1 &
p2 `1 <= s1 )
;
|[r1,r]| `1 = p2 `1
by A3, A5, A7, XXREAL_0:1;
then
p2 = |[r1,r]|
by A3, A7, Th11;
hence
x in {|[r1,r]|}
by A6, 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 A5, TOPREAL1:7;
:: thesis: verum end; suppose
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]|then A8:
s1 - r1 > 0
by XREAL_1:52;
let x be
set ;
:: 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 A9:
(
x = p2 &
p2 `2 = r &
r1 <= p2 `1 &
p2 `1 <= s1 )
;
set t =
p2 `1 ;
set l =
((p2 `1 ) - r1) / (s1 - r1);
(p2 `1 ) - r1 <= s1 - r1
by A9, XREAL_1:11;
then
(
((p2 `1 ) - r1) / (s1 - r1) <= (s1 - r1) / (s1 - r1) &
s1 - r1 <> 0 )
by A8, XREAL_1:74;
then A10:
((p2 `1 ) - r1) / (s1 - r1) <= 1
by XCMPLX_1:60;
(
r1 - r1 <= (p2 `1 ) - r1 &
r1 - r1 = 0 )
by A9, XREAL_1:11;
then A11:
(
0 / (s1 - r1) <= ((p2 `1 ) - r1) / (s1 - r1) &
s1 - r1 <> 0 )
by A8;
A12:
(((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 Th7
.=
((1 - (((p2 `1 ) - r1) / (s1 - r1))) * (|[r1,r]| `2 )) + (((((p2 `1 ) - r1) / (s1 - r1)) * |[s1,r]|) `2 )
by Th9
.=
((1 - (((p2 `1 ) - r1) / (s1 - r1))) * r) + ((((p2 `1 ) - r1) / (s1 - r1)) * r)
by A3, A4, Th9
.=
p2 `2
by A9
;
A13: 1
- (((p2 `1 ) - r1) / (s1 - r1)) =
((1 * (s1 - r1)) - ((p2 `1 ) - r1)) / (s1 - r1)
by A8, XCMPLX_1:128
.=
(s1 - (p2 `1 )) / (s1 - r1)
;
(((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 Th7
.=
((1 - (((p2 `1 ) - r1) / (s1 - r1))) * (|[r1,r]| `1 )) + (((((p2 `1 ) - r1) / (s1 - r1)) * |[s1,r]|) `1 )
by Th9
.=
((1 - (((p2 `1 ) - r1) / (s1 - r1))) * (|[r1,r]| `1 )) + ((((p2 `1 ) - r1) / (s1 - r1)) * (|[s1,r]| `1 ))
by Th9
.=
(((s1 - (p2 `1 )) * (|[r1,r]| `1 )) / (s1 - r1)) + ((((p2 `1 ) - r1) / (s1 - r1)) * (|[s1,r]| `1 ))
by A13, XCMPLX_1:75
.=
(((s1 - (p2 `1 )) * (|[r1,r]| `1 )) / (s1 - r1)) + ((((p2 `1 ) - r1) * (|[s1,r]| `1 )) / (s1 - r1))
by XCMPLX_1:75
.=
(((s1 * r1) - ((p2 `1 ) * r1)) + (((p2 `1 ) - r1) * s1)) / (s1 - r1)
by A3, A4, XCMPLX_1:63
.=
((p2 `1 ) * (s1 - r1)) / (s1 - r1)
.=
(p2 `1 ) * ((s1 - r1) / (s1 - r1))
by XCMPLX_1:75
.=
(p2 `1 ) * 1
by A8, XCMPLX_1:60
.=
p2 `1
;
then
p2 = ((1 - (((p2 `1 ) - r1) / (s1 - r1))) * |[r1,r]|) + ((((p2 `1 ) - r1) / (s1 - r1)) * |[s1,r]|)
by A12, Th11;
hence
x in LSeg |[r1,r]|,
|[s1,r]|
by A9, A10, A11;
:: thesis: verum end;
end;
let x be set ; :: 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
A14:
( ((1 - lambda) * |[r1,r]|) + (lambda * |[s1,r]|) = x & 0 <= lambda & lambda <= 1 )
;
set p2 = ((1 - lambda) * |[r1,r]|) + (lambda * |[s1,r]|);
A15: (((1 - lambda) * |[r1,r]|) + (lambda * |[s1,r]|)) `2 =
(((1 - lambda) * |[r1,r]|) `2 ) + ((lambda * |[s1,r]|) `2 )
by Th7
.=
((1 - lambda) * (|[r1,r]| `2 )) + ((lambda * |[s1,r]|) `2 )
by Th9
.=
((1 - lambda) * r) + (lambda * r)
by A3, A4, Th9
.=
r
;
A16: (((1 - lambda) * |[r1,r]|) + (lambda * |[s1,r]|)) `1 =
(((1 - lambda) * |[r1,r]|) `1 ) + ((lambda * |[s1,r]|) `1 )
by Th7
.=
((1 - lambda) * (|[r1,r]| `1 )) + ((lambda * |[s1,r]|) `1 )
by Th9
.=
((1 * r1) - (lambda * r1)) + (lambda * s1)
by A3, A4, Th9
.=
r1 + (lambda * (s1 - r1))
;
0 * (s1 - r1) <= lambda * (s1 - r1)
by A2, A14;
then A17:
r1 + 0 <= r1 + (lambda * (s1 - r1))
by XREAL_1:9;
lambda * (s1 - r1) <= 1 * (s1 - r1)
by A2, A14, XREAL_1:66;
then
r1 + (lambda * (s1 - r1)) <= (s1 - r1) + r1
by XREAL_1:9;
hence
x in { p3 where p3 is Point of (TOP-REAL 2) : ( p3 `2 = r & r1 <= p3 `1 & p3 `1 <= s1 ) }
by A14, A15, A16, A17; :: thesis: verum