theorem :: TOPGEN_3:12

for x, y being Real holds ].x,y.[ is open Subset of Sorgenfrey-line