theorem Th25: :: COUSIN:28

for a, b being Real
for S being Subset of (Euclid 1) st a <= b & S = product <*[.a,b.]*> holds
diameter S = b - a