let s1, t1, s2, t2 be Real; for P, Q being Subset of (TOP-REAL 2) st P = { p where p is Point of (TOP-REAL 2) : ( s1 < p `1 & p `1 < s2 & t1 < p `2 & p `2 < t2 ) } & Q = { qc where qc is Point of (TOP-REAL 2) : ( not s1 <= qc `1 or not qc `1 <= s2 or not t1 <= qc `2 or not qc `2 <= t2 ) } holds
P misses Q
let P, Q be Subset of (TOP-REAL 2); ( P = { p where p is Point of (TOP-REAL 2) : ( s1 < p `1 & p `1 < s2 & t1 < p `2 & p `2 < t2 ) } & Q = { qc where qc is Point of (TOP-REAL 2) : ( not s1 <= qc `1 or not qc `1 <= s2 or not t1 <= qc `2 or not qc `2 <= t2 ) } implies P misses Q )
assume that
A1:
P = { p where p is Point of (TOP-REAL 2) : ( s1 < p `1 & p `1 < s2 & t1 < p `2 & p `2 < t2 ) }
and
A2:
Q = { qc where qc is Point of (TOP-REAL 2) : ( not s1 <= qc `1 or not qc `1 <= s2 or not t1 <= qc `2 or not qc `2 <= t2 ) }
; P misses Q
A3:
P = { |[sa,ta]| where sa, ta is Real : ( s1 < sa & sa < s2 & t1 < ta & ta < t2 ) }
by A1, Th21;
Q = { |[sb,tb]| where sb, tb is Real : ( not s1 <= sb or not sb <= s2 or not t1 <= tb or not tb <= t2 ) }
by A2, Th22;
hence
P misses Q
by A3, Th20; verum