theorem Th20: :: COUSIN:23

for a, b being 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