let r, r1, s1 be Real; ( 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]|;
A1:
|[r1,r]| `1 = r1
by EUCLID:52;
assume A2:
r1 <= s1
; { 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
by EUCLID:52;
A5:
|[r1,r]| `2 = r
by EUCLID:52;
A6:
|[s1,r]| `1 = s1
by EUCLID:52;
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]|)
XBOOLE_0:def 10 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
;
{ 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 ;
TARSKI:def 3 ( 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 ) }
;
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 A1, A7, A10, XXREAL_0:1;
then
p2 = |[r1,r]|
by A5, A9, Th6;
hence
x in {|[r1,r]|}
by A8, TARSKI:def 1;
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;
verum end; suppose A11:
r1 < s1
;
{ 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 ;
TARSKI:def 3 ( 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 ) }
;
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 A5, 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 A1, A6, 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;
verum end;
end;
let x be object ; TARSKI:def 3 ( 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]|)
; 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 A1, 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 A5, 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; verum