let a, b be Real; for S being Subset of (Euclid 1) st a <= b & S = product <*[.a,b.]*> holds
for x, y being Point of (Euclid 1) st x in S & y in S holds
dist (x,y) <= b - a
let S be Subset of (Euclid 1); ( a <= b & S = product <*[.a,b.]*> implies for x, y being Point of (Euclid 1) st x in S & y in S holds
dist (x,y) <= b - a )
assume that
A1:
a <= b
and
A2:
S = product <*[.a,b.]*>
; for x, y being Point of (Euclid 1) st x in S & y in S holds
dist (x,y) <= b - a
set si = product <*[.a,b.]*>;
reconsider si = product <*[.a,b.]*> as Subset of (Euclid 1) by A2;
set r = b - a;
for x, y being Point of (Euclid 1) st x in si & y in si holds
dist (x,y) <= b - a
proof
set r =
b - a;
per cases
( b - a = 0 or 0 < b - a )
by A1, XREAL_1:48;
suppose
0 < b - a
;
for x, y being Point of (Euclid 1) st x in si & y in si holds
dist (x,y) <= b - ahereby verum
let x,
y be
Point of
(Euclid 1);
( x in si & y in si implies dist (x,y) <= b - a )assume that A6:
x in si
and A7:
y in si
;
dist (x,y) <= b - aconsider gx being
Function such that A8:
x = gx
and
dom gx = dom <*[.a,b.]*>
and A9:
for
j being
object st
j in dom <*[.a,b.]*> holds
gx . j in <*[.a,b.]*> . j
by A6, CARD_3:def 5;
consider gy being
Function such that A10:
y = gy
and
dom gy = dom <*[.a,b.]*>
and A11:
for
j being
object st
j in dom <*[.a,b.]*> holds
gy . j in <*[.a,b.]*> . j
by A7, CARD_3:def 5;
(
x in Euclid 1 &
y in Euclid 1 )
;
then
(
x in TOP-REAL 1 &
y in TOP-REAL 1 )
by EUCLID:67;
then reconsider rx =
x,
ry =
y as
Element of
REAL 1
by EUCLID:22;
Euclid 1
= MetrStruct(#
(REAL 1),
(Pitag_dist 1) #)
by EUCLID:def 7;
then A12:
dist (
x,
y)
= |.(rx - ry).|
by EUCLID:def 6;
consider ux being
Real such that A13:
rx = <*ux*>
by Th6;
consider uy being
Real such that A14:
ry = <*uy*>
by Th6;
(
rx = 1
|-> ux &
ry = 1
|-> uy )
by A13, A14, FINSEQ_2:59;
then A15:
|.(rx - ry).| =
(sqrt 1) * |.(ux - uy).|
by TOPREALC:11
.=
|.(ux - uy).|
by SQUARE_1:18
;
1
in Seg 1
by TARSKI:def 1, FINSEQ_1:2;
then
1
in dom <*[.a,b.]*>
by FINSEQ_1:def 8;
then
(
gx . 1
in <*[.a,b.]*> . 1 &
gy . 1
in <*[.a,b.]*> . 1 )
by A9, A11;
then
(
gx . 1
in [.a,b.] &
gy . 1
in [.a,b.] )
by FINSEQ_1:def 8;
then
(
ux in [.a,b.] &
uy in [.a,b.] )
by A8, A10, A13, A14, FINSEQ_1:def 8;
hence
dist (
x,
y)
<= b - a
by A12, A15, UNIFORM1:12;
verum
end; end; end;
end;
hence
for x, y being Point of (Euclid 1) st x in S & y in S holds
dist (x,y) <= b - a
by A2; verum