theorem Th20: :: JORDAN1:26

for s1, t1, s2, t2 being Real
for P, Q being Subset of (TOP-REAL 2) st P = { |[sa,ta]| where sa, ta is Real : ( s1 < sa & sa < s2 & t1 < ta & ta < t2 ) } & Q = { |[sb,tb]| where sb, tb is Real : ( not s1 <= sb or not sb <= s2 or not t1 <= tb or not tb <= t2 ) } holds
P misses Q