let a, b be Real; :: thesis: 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); :: thesis: ( a <= b & S = product <*[.a,b.]*> implies diameter S = b - a )
assume that
A1: a <= b and
A2: S = product <*[.a,b.]*> ; :: thesis: 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; :: thesis: 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 :: thesis: verum

proof

let s be Real; :: thesis: ( ( 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 ; :: thesis: b - a <= s
assume A6: s < b - a ; :: thesis: 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; :: thesis: verum

end;

end;

hence diameter S = b - a by A3, A4, TBSP_1:def 8; :: thesis: verum