theorem Th57: :: TOPGEN_5:57

for x, y being Real holds [.x,y.[ is closed Subset of Sorgenfrey-line