let r, r1, s1 be Real; ( 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]|) )
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]|;
A1:
|[r,r1]| `1 = r
by EUCLID:52;
assume A2:
r1 <= s1
; { p1 where p1 is Point of (TOP-REAL 2) : ( p1 `1 = r & r1 <= p1 `2 & p1 `2 <= s1 ) } = LSeg (|[r,r1]|,|[r,s1]|)
then A3:
s1 - r1 >= r1 - r1
by XREAL_1:13;
A4:
|[r,s1]| `2 = s1
by EUCLID:52;
A5:
|[r,r1]| `2 = r1
by EUCLID:52;
A6:
|[r,s1]| `1 = r
by EUCLID:52;
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]|)
XBOOLE_0:def 10 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 A2, XXREAL_0:1;
suppose A7:
r1 = s1
;
{ 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
object ;
TARSKI:def 3 ( 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 ) }
;
x in {|[r,r1]|}
then consider p2 being
Point of
(TOP-REAL 2) such that A8:
x = p2
and A9:
p2 `1 = r
and A10:
(
r1 <= p2 `2 &
p2 `2 <= s1 )
;
|[r,r1]| `2 = p2 `2
by A5, A7, A10, XXREAL_0:1;
then
p2 = |[r,r1]|
by A1, A9, Th6;
hence
x in {|[r,r1]|}
by A8, TARSKI:def 1;
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 A7, RLTOPSP1:70;
verum end; suppose A11:
r1 < s1
;
{ p3 where p3 is Point of (TOP-REAL 2) : ( p3 `1 = r & r1 <= p3 `2 & p3 `2 <= s1 ) } c= LSeg (|[r,r1]|,|[r,s1]|)let x be
object ;
TARSKI:def 3 ( 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 ) }
;
x in LSeg (|[r,r1]|,|[r,s1]|)then consider p2 being
Point of
(TOP-REAL 2) such that A12:
x = p2
and A13:
p2 `1 = r
and A14:
r1 <= p2 `2
and A15:
p2 `2 <= s1
;
set t =
p2 `2 ;
set l =
((p2 `2) - r1) / (s1 - r1);
A16:
s1 - r1 > 0
by A11, XREAL_1:50;
then A17: 1
- (((p2 `2) - r1) / (s1 - r1)) =
((1 * (s1 - r1)) - ((p2 `2) - r1)) / (s1 - r1)
by XCMPLX_1:127
.=
(s1 - (p2 `2)) / (s1 - r1)
;
(p2 `2) - r1 <= s1 - r1
by A15, XREAL_1:9;
then
((p2 `2) - r1) / (s1 - r1) <= (s1 - r1) / (s1 - r1)
by A16, XREAL_1:72;
then A18:
((p2 `2) - r1) / (s1 - r1) <= 1
by A16, XCMPLX_1:60;
A19:
(((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 Th2
.=
((1 - (((p2 `2) - r1) / (s1 - r1))) * (|[r,r1]| `1)) + (((((p2 `2) - r1) / (s1 - r1)) * |[r,s1]|) `1)
by Th4
.=
((1 - (((p2 `2) - r1) / (s1 - r1))) * r) + ((((p2 `2) - r1) / (s1 - r1)) * r)
by A1, A6, Th4
.=
p2 `1
by A13
;
(((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 Th2
.=
((1 - (((p2 `2) - r1) / (s1 - r1))) * (|[r,r1]| `2)) + (((((p2 `2) - r1) / (s1 - r1)) * |[r,s1]|) `2)
by Th4
.=
((1 - (((p2 `2) - r1) / (s1 - r1))) * (|[r,r1]| `2)) + ((((p2 `2) - r1) / (s1 - r1)) * (|[r,s1]| `2))
by Th4
.=
(((s1 - (p2 `2)) * (|[r,r1]| `2)) / (s1 - r1)) + ((((p2 `2) - r1) / (s1 - r1)) * (|[r,s1]| `2))
by A17, XCMPLX_1:74
.=
(((s1 - (p2 `2)) * (|[r,r1]| `2)) / (s1 - r1)) + ((((p2 `2) - r1) * (|[r,s1]| `2)) / (s1 - r1))
by XCMPLX_1:74
.=
(((s1 * r1) - ((p2 `2) * r1)) + (((p2 `2) - r1) * s1)) / (s1 - r1)
by A5, A4, XCMPLX_1:62
.=
((p2 `2) * (s1 - r1)) / (s1 - r1)
.=
(p2 `2) * ((s1 - r1) / (s1 - r1))
by XCMPLX_1:74
.=
(p2 `2) * 1
by A16, XCMPLX_1:60
.=
p2 `2
;
then A20:
p2 = ((1 - (((p2 `2) - r1) / (s1 - r1))) * |[r,r1]|) + ((((p2 `2) - r1) / (s1 - r1)) * |[r,s1]|)
by A19, Th6;
r1 - r1 <= (p2 `2) - r1
by A14, XREAL_1:9;
hence
x in LSeg (
|[r,r1]|,
|[r,s1]|)
by A16, A12, A18, A20;
verum end; end;
end;
let x be object ; TARSKI:def 3 ( 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]|)
; 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
A21:
((1 - lambda) * |[r,r1]|) + (lambda * |[r,s1]|) = 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) * |[r,r1]|) + (lambda * |[r,s1]|);
A26: (((1 - lambda) * |[r,r1]|) + (lambda * |[r,s1]|)) `2 =
(((1 - lambda) * |[r,r1]|) `2) + ((lambda * |[r,s1]|) `2)
by Th2
.=
((1 - lambda) * (|[r,r1]| `2)) + ((lambda * |[r,s1]|) `2)
by Th4
.=
((1 * r1) - (lambda * r1)) + (lambda * s1)
by A5, A4, Th4
.=
r1 + (lambda * (s1 - r1))
;
(((1 - lambda) * |[r,r1]|) + (lambda * |[r,s1]|)) `1 =
(((1 - lambda) * |[r,r1]|) `1) + ((lambda * |[r,s1]|) `1)
by Th2
.=
((1 - lambda) * (|[r,r1]| `1)) + ((lambda * |[r,s1]|) `1)
by Th4
.=
((1 - lambda) * r) + (lambda * r)
by A1, A6, Th4
.=
1 * r
;
hence
x in { p1 where p1 is Point of (TOP-REAL 2) : ( p1 `1 = r & r1 <= p1 `2 & p1 `2 <= s1 ) }
by A21, A26, A24, A25; verum