let s1, t1, s2, t2 be Real; :: thesis: 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
let P, Q be Subset of (TOP-REAL 2); :: thesis: ( 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 ) } implies P misses Q )
assume that
A1: P = { |[sa,ta]| where sa, ta is Real : ( s1 < sa & sa < s2 & t1 < ta & ta < t2 ) } and
A2: Q = { |[sb,tb]| where sb, tb is Real : ( not s1 <= sb or not sb <= s2 or not t1 <= tb or not tb <= t2 ) } ; :: thesis: P misses Q
assume not P misses Q ; :: thesis: contradiction
then consider x being object such that
A3: x in P and
A4: x in Q by XBOOLE_0:3;
consider sa, ta being Real such that
A5: |[sa,ta]| = x and
A6: s1 < sa and
A7: sa < s2 and
A8: t1 < ta and
A9: ta < t2 by A1, A3;
A10: ex sb, tb being Real st
( |[sb,tb]| = x & ( not s1 <= sb or not sb <= s2 or not t1 <= tb or not tb <= t2 ) ) by A2, A4;
set p = |[sa,ta]|;
A11: |[sa,ta]| `1 = sa by EUCLID:52;
|[sa,ta]| `2 = ta by EUCLID:52;
hence contradiction by A5, A6, A7, A8, A9, A10, A11, EUCLID:52; :: thesis: verum