let p be Point of (TOP-REAL 2); :: thesis: for X being non empty compact Subset of (TOP-REAL 2) st p in X holds
( lower_bound (proj1 | X) <= p `1 & p `1 <= upper_bound (proj1 | X) & lower_bound (proj2 | X) <= p `2 & p `2 <= upper_bound (proj2 | X) )
let X be non empty compact Subset of (TOP-REAL 2); :: thesis: ( p in X implies ( lower_bound (proj1 | X) <= p `1 & p `1 <= upper_bound (proj1 | X) & lower_bound (proj2 | X) <= p `2 & p `2 <= upper_bound (proj2 | X) ) )
assume A1: p in X ; :: thesis: ( lower_bound (proj1 | X) <= p `1 & p `1 <= upper_bound (proj1 | X) & lower_bound (proj2 | X) <= p `2 & p `2 <= upper_bound (proj2 | X) )
then reconsider p9 = p as Point of ((TOP-REAL 2) | X) by PRE_TOPC:8;
A2: (proj1 | X) . p9 = p `1 by A1, Th22;
hence lower_bound (proj1 | X) <= p `1 by Th1; :: thesis: ( p `1 <= upper_bound (proj1 | X) & lower_bound (proj2 | X) <= p `2 & p `2 <= upper_bound (proj2 | X) )
thus p `1 <= upper_bound (proj1 | X) by A2, Th4; :: thesis: ( lower_bound (proj2 | X) <= p `2 & p `2 <= upper_bound (proj2 | X) )
A3: (proj2 | X) . p9 = p `2 by A1, Th23;
hence lower_bound (proj2 | X) <= p `2 by Th1; :: thesis: p `2 <= upper_bound (proj2 | X)
thus p `2 <= upper_bound (proj2 | X) by A3, Th4; :: thesis: verum