theorem Th19: :: JORDAN1:25

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