let s1, t1, s2, t2 be Real; :: thesis: for P being Subset of (TOP-REAL 2) st P = { p0 where p0 is Point of (TOP-REAL 2) : ( s1 < p0 `1 & p0 `1 < s2 & t1 < p0 `2 & p0 `2 < t2 ) } holds
P is open
let P be Subset of (TOP-REAL 2); :: thesis: ( P = { p0 where p0 is Point of (TOP-REAL 2) : ( s1 < p0 `1 & p0 `1 < s2 & t1 < p0 `2 & p0 `2 < t2 ) } implies P is open )
assume P = { p0 where p0 is Point of (TOP-REAL 2) : ( s1 < p0 `1 & p0 `1 < s2 & t1 < p0 `2 & p0 `2 < t2 ) } ; :: thesis: P is open
then P = { |[sa,ta]| where sa, ta is Real : ( s1 < sa & sa < s2 & t1 < ta & ta < t2 ) } by Th21;
hence P is open by Th18; :: thesis: verum