theorem Th18: :: JORDAN1:24

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