theorem :: TOPGEN_5:55

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