let p be Point of (TOP-REAL 2); :: thesis: for X being Subset of (TOP-REAL 2) st p in X & X is Bounded holds
( inf (proj2 | X) <= p `2 & p `2 <= sup (proj2 | X) )
let X be Subset of (TOP-REAL 2); :: thesis: ( p in X & X is Bounded implies ( inf (proj2 | X) <= p `2 & p `2 <= sup (proj2 | X) ) )
set T = TOP-REAL 2;
assume A1: ( p in X & X is Bounded ) ; :: thesis: ( inf (proj2 | X) <= p `2 & p `2 <= sup (proj2 | X) )
then reconsider X = X as non empty Subset of (TOP-REAL 2) ;
reconsider p' = p as Point of ((TOP-REAL 2) | X) by A1, PRE_TOPC:29;
A2: the carrier of ((TOP-REAL 2) | X) = X by PRE_TOPC:29;
A3: (proj2 | X) .: X = proj2 .: X by RELAT_1:162;
A4: proj2 .: X is bounded by A1, JCT_MISC:23;
then A5: (proj2 | X) .: X is bounded_above by A3, XXREAL_2:def 11;
(proj2 | X) .: X is bounded_below by A3, A4, XXREAL_2:def 11;
then A6: proj2 | X is bounded_below by A2, PSCOMP_1:def 11;
proj2 | X is bounded_above by A2, A5, PSCOMP_1:def 12;
then reconsider f = proj2 | X as bounded RealMap of ((TOP-REAL 2) | X) by A6;
(proj2 | X) . p' = p `2 by A1, PSCOMP_1:70;
then ( inf f <= p `2 & p `2 <= sup f ) by PSCOMP_1:47, PSCOMP_1:50;
hence ( inf (proj2 | X) <= p `2 & p `2 <= sup (proj2 | X) ) ; :: thesis: verum