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 (proj1 | X) <= p `1 & p `1 <= sup (proj1 | X) )
let X be Subset of (TOP-REAL 2); :: thesis: ( p in X & X is Bounded implies ( inf (proj1 | X) <= p `1 & p `1 <= sup (proj1 | X) ) )
set T = TOP-REAL 2;
assume A1: ( p in X & X is Bounded ) ; :: thesis: ( inf (proj1 | X) <= p `1 & p `1 <= sup (proj1 | 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: (proj1 | X) .: X = proj1 .: X by RELAT_1:162;
A4: proj1 .: X is bounded by A1, Th4;
then A5: (proj1 | X) .: X is bounded_above by A3, XXREAL_2:def 11;
(proj1 | X) .: X is bounded_below by A3, A4, XXREAL_2:def 11;
then A6: proj1 | X is bounded_below by A2, PSCOMP_1:def 11;
proj1 | X is bounded_above by A2, A5, PSCOMP_1:def 12;
then reconsider f = proj1 | X as bounded RealMap of ((TOP-REAL 2) | X) by A6;
(proj1 | X) . p' = p `1 by A1, PSCOMP_1:69;
then ( inf f <= p `1 & p `1 <= sup f ) by PSCOMP_1:47, PSCOMP_1:50;
hence ( inf (proj1 | X) <= p `1 & p `1 <= sup (proj1 | X) ) ; :: thesis: verum