theorem Th14: :: JORDAN1:20

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