theorem Th17: :: JORDAN1:23

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