let r1, s1, r be real number ; :: thesis: ( r1 <= s1 implies { p1 where p1 is Point of (TOP-REAL 2) : ( p1 `1 = r & r1 <= p1 `2 & p1 `2 <= s1 ) } = LSeg |[r,r1]|,|[r,s1]| )
assume A1:
r1 <= s1
; :: thesis: { p1 where p1 is Point of (TOP-REAL 2) : ( p1 `1 = r & r1 <= p1 `2 & p1 `2 <= s1 ) } = LSeg |[r,r1]|,|[r,s1]|
then A2:
s1 - r1 >= r1 - r1
by XREAL_1:15;
set L = { p3 where p3 is Point of (TOP-REAL 2) : ( p3 `1 = r & r1 <= p3 `2 & p3 `2 <= s1 ) } ;
set p = |[r,r1]|;
set q = |[r,s1]|;
A3:
( |[r,r1]| `1 = r & |[r,r1]| `2 = r1 )
by EUCLID:56;
A4:
( |[r,s1]| `1 = r & |[r,s1]| `2 = s1 )
by EUCLID:56;
thus
{ p3 where p3 is Point of (TOP-REAL 2) : ( p3 `1 = r & r1 <= p3 `2 & p3 `2 <= s1 ) } c= LSeg |[r,r1]|,|[r,s1]|
:: according to XBOOLE_0:def 10 :: thesis: LSeg |[r,r1]|,|[r,s1]| c= { p1 where p1 is Point of (TOP-REAL 2) : ( p1 `1 = r & r1 <= p1 `2 & p1 `2 <= 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 `1 = r & r1 <= p3 `2 & p3 `2 <= s1 ) } c= LSeg |[r,r1]|,|[r,s1]|
{ p3 where p3 is Point of (TOP-REAL 2) : ( p3 `1 = r & r1 <= p3 `2 & p3 `2 <= s1 ) } c= {|[r,r1]|}
proof
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in { p3 where p3 is Point of (TOP-REAL 2) : ( p3 `1 = r & r1 <= p3 `2 & p3 `2 <= s1 ) } or x in {|[r,r1]|} )
assume
x in { p3 where p3 is Point of (TOP-REAL 2) : ( p3 `1 = r & r1 <= p3 `2 & p3 `2 <= s1 ) }
;
:: thesis: x in {|[r,r1]|}
then consider p2 being
Point of
(TOP-REAL 2) such that A6:
x = p2
and A7:
(
p2 `1 = r &
r1 <= p2 `2 &
p2 `2 <= s1 )
;
|[r,r1]| `2 = p2 `2
by A3, A5, A7, XXREAL_0:1;
then
p2 = |[r,r1]|
by A3, A7, Th11;
hence
x in {|[r,r1]|}
by A6, TARSKI:def 1;
:: thesis: verum
end; hence
{ p3 where p3 is Point of (TOP-REAL 2) : ( p3 `1 = r & r1 <= p3 `2 & p3 `2 <= s1 ) } c= LSeg |[r,r1]|,
|[r,s1]|
by A5, TOPREAL1:7;
:: thesis: verum end; suppose
r1 < s1
;
:: thesis: { p3 where p3 is Point of (TOP-REAL 2) : ( p3 `1 = r & r1 <= p3 `2 & p3 `2 <= s1 ) } c= LSeg |[r,r1]|,|[r,s1]|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 `1 = r & r1 <= p3 `2 & p3 `2 <= s1 ) } or x in LSeg |[r,r1]|,|[r,s1]| )assume
x in { p3 where p3 is Point of (TOP-REAL 2) : ( p3 `1 = r & r1 <= p3 `2 & p3 `2 <= s1 ) }
;
:: thesis: x in LSeg |[r,r1]|,|[r,s1]|then consider p2 being
Point of
(TOP-REAL 2) such that A9:
(
x = p2 &
p2 `1 = r &
r1 <= p2 `2 &
p2 `2 <= s1 )
;
set t =
p2 `2 ;
set l =
((p2 `2 ) - r1) / (s1 - r1);
(p2 `2 ) - r1 <= s1 - r1
by A9, XREAL_1:11;
then
(
((p2 `2 ) - r1) / (s1 - r1) <= (s1 - r1) / (s1 - r1) &
s1 - r1 <> 0 )
by A8, XREAL_1:74;
then A10:
((p2 `2 ) - r1) / (s1 - r1) <= 1
by XCMPLX_1:60;
(
r1 - r1 <= (p2 `2 ) - r1 &
r1 - r1 = 0 )
by A9, XREAL_1:11;
then A11:
(
0 / (s1 - r1) <= ((p2 `2 ) - r1) / (s1 - r1) &
s1 - r1 <> 0 )
by A8;
A12:
(((1 - (((p2 `2 ) - r1) / (s1 - r1))) * |[r,r1]|) + ((((p2 `2 ) - r1) / (s1 - r1)) * |[r,s1]|)) `1 =
(((1 - (((p2 `2 ) - r1) / (s1 - r1))) * |[r,r1]|) `1 ) + (((((p2 `2 ) - r1) / (s1 - r1)) * |[r,s1]|) `1 )
by Th7
.=
((1 - (((p2 `2 ) - r1) / (s1 - r1))) * (|[r,r1]| `1 )) + (((((p2 `2 ) - r1) / (s1 - r1)) * |[r,s1]|) `1 )
by Th9
.=
((1 - (((p2 `2 ) - r1) / (s1 - r1))) * r) + ((((p2 `2 ) - r1) / (s1 - r1)) * r)
by A3, A4, Th9
.=
p2 `1
by A9
;
A13: 1
- (((p2 `2 ) - r1) / (s1 - r1)) =
((1 * (s1 - r1)) - ((p2 `2 ) - r1)) / (s1 - r1)
by A8, XCMPLX_1:128
.=
(s1 - (p2 `2 )) / (s1 - r1)
;
(((1 - (((p2 `2 ) - r1) / (s1 - r1))) * |[r,r1]|) + ((((p2 `2 ) - r1) / (s1 - r1)) * |[r,s1]|)) `2 =
(((1 - (((p2 `2 ) - r1) / (s1 - r1))) * |[r,r1]|) `2 ) + (((((p2 `2 ) - r1) / (s1 - r1)) * |[r,s1]|) `2 )
by Th7
.=
((1 - (((p2 `2 ) - r1) / (s1 - r1))) * (|[r,r1]| `2 )) + (((((p2 `2 ) - r1) / (s1 - r1)) * |[r,s1]|) `2 )
by Th9
.=
((1 - (((p2 `2 ) - r1) / (s1 - r1))) * (|[r,r1]| `2 )) + ((((p2 `2 ) - r1) / (s1 - r1)) * (|[r,s1]| `2 ))
by Th9
.=
(((s1 - (p2 `2 )) * (|[r,r1]| `2 )) / (s1 - r1)) + ((((p2 `2 ) - r1) / (s1 - r1)) * (|[r,s1]| `2 ))
by A13, XCMPLX_1:75
.=
(((s1 - (p2 `2 )) * (|[r,r1]| `2 )) / (s1 - r1)) + ((((p2 `2 ) - r1) * (|[r,s1]| `2 )) / (s1 - r1))
by XCMPLX_1:75
.=
(((s1 * r1) - ((p2 `2 ) * r1)) + (((p2 `2 ) - r1) * s1)) / (s1 - r1)
by A3, A4, XCMPLX_1:63
.=
((p2 `2 ) * (s1 - r1)) / (s1 - r1)
.=
(p2 `2 ) * ((s1 - r1) / (s1 - r1))
by XCMPLX_1:75
.=
(p2 `2 ) * 1
by A8, XCMPLX_1:60
.=
p2 `2
;
then
p2 = ((1 - (((p2 `2 ) - r1) / (s1 - r1))) * |[r,r1]|) + ((((p2 `2 ) - r1) / (s1 - r1)) * |[r,s1]|)
by A12, Th11;
hence
x in LSeg |[r,r1]|,
|[r,s1]|
by A9, A10, A11;
:: thesis: verum end;
end;
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in LSeg |[r,r1]|,|[r,s1]| or x in { p1 where p1 is Point of (TOP-REAL 2) : ( p1 `1 = r & r1 <= p1 `2 & p1 `2 <= s1 ) } )
assume
x in LSeg |[r,r1]|,|[r,s1]|
; :: thesis: x in { p1 where p1 is Point of (TOP-REAL 2) : ( p1 `1 = r & r1 <= p1 `2 & p1 `2 <= s1 ) }
then consider lambda being Real such that
A14:
( ((1 - lambda) * |[r,r1]|) + (lambda * |[r,s1]|) = x & 0 <= lambda & lambda <= 1 )
;
set p2 = ((1 - lambda) * |[r,r1]|) + (lambda * |[r,s1]|);
A15: (((1 - lambda) * |[r,r1]|) + (lambda * |[r,s1]|)) `1 =
(((1 - lambda) * |[r,r1]|) `1 ) + ((lambda * |[r,s1]|) `1 )
by Th7
.=
((1 - lambda) * (|[r,r1]| `1 )) + ((lambda * |[r,s1]|) `1 )
by Th9
.=
((1 - lambda) * r) + (lambda * r)
by A3, A4, Th9
.=
1 * r
;
A16: (((1 - lambda) * |[r,r1]|) + (lambda * |[r,s1]|)) `2 =
(((1 - lambda) * |[r,r1]|) `2 ) + ((lambda * |[r,s1]|) `2 )
by Th7
.=
((1 - lambda) * (|[r,r1]| `2 )) + ((lambda * |[r,s1]|) `2 )
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 `1 = r & r1 <= p3 `2 & p3 `2 <= s1 ) }
by A14, A15, A16, A17; :: thesis: verum