theorem Th54: :: TOPGEN_5:54

for x being Real holds left_open_halfline x is closed Subset of Sorgenfrey-line