let s1, s2, t1, t2 be Real; :: thesis: { p0 where p0 is Point of (TOP-REAL 2) : ( s1 < p0 `1 & p0 `1 < s2 & t1 < p0 `2 & p0 `2 < t2 ) } is Subset of (TOP-REAL 2)
{ |[sc,tc]| where sc, tc is Real : ( s1 < sc & sc < s2 & t1 < tc & tc < t2 ) } is Subset of (TOP-REAL 2) by Lm2, Lm7;
hence { p0 where p0 is Point of (TOP-REAL 2) : ( s1 < p0 `1 & p0 `1 < s2 & t1 < p0 `2 & p0 `2 < t2 ) } is Subset of (TOP-REAL 2) by Th21; :: thesis: verum