theorem :: TOPGEN_3:15

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