theorem :: TOPGEN_3:13

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