theorem Th16: :: JORDAN1:22

for s1 being Real holds { |[s,t]| where s, t is Real : s1 < t } is open Subset of (TOP-REAL 2)