let a, b be Real; for S being Subset of (Euclid 1) st a <= b & S = product <*[.a,b.]*> holds
diameter S = b - a
let S be Subset of (Euclid 1); ( a <= b & S = product <*[.a,b.]*> implies diameter S = b - a )
assume that
A1:
a <= b
and
A2:
S = product <*[.a,b.]*>
; diameter S = b - a
set f = <*[.a,b.]*>;
A3:
S is bounded
by A1, A2, Th21;
A4:
not S is empty
by A1, A2, Th24;
( ( for x, y being Point of (Euclid 1) st x in S & y in S holds
dist (x,y) <= b - a ) & ( for s being Real st ( for x, y being Point of (Euclid 1) st x in S & y in S holds
dist (x,y) <= s ) holds
b - a <= s ) )
proof
thus
for
x,
y being
Point of
(Euclid 1) st
x in S &
y in S holds
dist (
x,
y)
<= b - a
by A1, A2, Th20;
for s being Real st ( for x, y being Point of (Euclid 1) st x in S & y in S holds
dist (x,y) <= s ) holds
b - a <= s
thus
for
s being
Real st ( for
x,
y being
Point of
(Euclid 1) st
x in S &
y in S holds
dist (
x,
y)
<= s ) holds
b - a <= s
verumproof
let s be
Real;
( ( for x, y being Point of (Euclid 1) st x in S & y in S holds
dist (x,y) <= s ) implies b - a <= s )
assume A5:
for
x,
y being
Point of
(Euclid 1) st
x in S &
y in S holds
dist (
x,
y)
<= s
;
b - a <= s
assume A6:
s < b - a
;
contradiction
A7:
(
<*a*> in S &
<*b*> in S )
by A2, A1, Th24;
reconsider sa =
<*a*>,
sb =
<*b*> as
Point of
(Euclid 1) by Th7;
A8:
dist (
sa,
sb)
<= s
by A5, A7;
a - a <= b - a
by A1, XREAL_1:9;
then
|.(b - a).| = b - a
by ABSVALUE:def 1;
hence
contradiction
by A6, A8, Th19;
verum
end;
end;
hence
diameter S = b - a
by A3, A4, TBSP_1:def 8; verum