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
( inf (proj1 | X) <= p `1 & p `1 <= sup (proj1 | X) & inf (proj2 | X) <= p `2 & p `2 <= sup (proj2 | X) )
let X be non empty compact Subset of (TOP-REAL 2); :: thesis: ( p in X implies ( inf (proj1 | X) <= p `1 & p `1 <= sup (proj1 | X) & inf (proj2 | X) <= p `2 & p `2 <= sup (proj2 | X) ) )
assume A1: p in X ; :: thesis: ( inf (proj1 | X) <= p `1 & p `1 <= sup (proj1 | X) & inf (proj2 | X) <= p `2 & p `2 <= sup (proj2 | X) )
then reconsider p' = p as Point of ((TOP-REAL 2) | X) by PRE_TOPC:29;
A2: (proj1 | X) . p' = p `1 by A1, Th69;
hence inf (proj1 | X) <= p `1 by Th47; :: thesis: ( p `1 <= sup (proj1 | X) & inf (proj2 | X) <= p `2 & p `2 <= sup (proj2 | X) )
thus p `1 <= sup (proj1 | X) by A2, Th50; :: thesis: ( inf (proj2 | X) <= p `2 & p `2 <= sup (proj2 | X) )
A3: (proj2 | X) . p' = p `2 by A1, Th70;
hence inf (proj2 | X) <= p `2 by Th47; :: thesis: p `2 <= sup (proj2 | X)
thus p `2 <= sup (proj2 | X) by A3, Th50; :: thesis: verum