let s1, t1, s2, t2 be Real; :: thesis: 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); :: thesis: ( 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 ) } ; :: thesis: 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; :: thesis: verum