theorem :: TOPGEN_3:14

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