let a, b be Real; :: thesis: 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); :: thesis: ( 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.]*> ; :: thesis: 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 A3: b - a = 0 ; :: thesis: for x, y being Point of (Euclid 1) st x in si & y in si holds
dist (x,y) <= b - a

then A4: product <*[.a,b.]*> = product <*{a}*> by XXREAL_1:17
.= {<*a*>} by Th5 ;

now :: thesis: for x, y being Point of (Euclid 1) st x in si & y in si holds
dist (x,y) <= b - a

set r = b - a;

hereby :: thesis: verum

let x, y be Point of (Euclid 1); :: thesis: ( x in si & y in si implies dist (x,y) <= b - a )
assume ( x in si & y in si ) ; :: thesis: dist (x,y) <= b - a
then A5: ( x = <*a*> & y = <*a*> ) by A4, TARSKI:def 1;
Euclid 1 is Reflexive ;
hence dist (x,y) <= b - a by A3, A5, METRIC_1:def 2; :: thesis: verum

end;

end;

hence for x, y being Point of (Euclid 1) st x in si & y in si holds
dist (x,y) <= b - a ; :: thesis: verum

end;

suppose 0 < b - a ; :: thesis: for x, y being Point of (Euclid 1) st x in si & y in si holds
dist (x,y) <= b - a

hereby :: thesis: verum

let x, y be Point of (Euclid 1); :: thesis: ( x in si & y in si implies dist (x,y) <= b - a )
assume that
A6: x in si and
A7: y in si ; :: thesis: dist (x,y) <= b - a
consider 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.] ) ;
then ( ux in [.a,b.] & uy in [.a,b.] ) by A8, A10, A13, A14;
hence dist (x,y) <= b - a by A12, A15, UNIFORM1:12; :: thesis: 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; :: thesis: verum