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