theorem Th15: :: JORDAN1:21

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