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
( lower_bound (proj1 | X) <= p `1 & p `1 <= upper_bound (proj1 | X) )
set T = TOP-REAL 2;
let X be Subset of (TOP-REAL 2); :: thesis: ( p in X & X is bounded implies ( lower_bound (proj1 | X) <= p `1 & p `1 <= upper_bound (proj1 | X) ) )
assume that
A1: p in X and
A2: X is bounded ; :: thesis: ( lower_bound (proj1 | X) <= p `1 & p `1 <= upper_bound (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:8;
A4: (proj1 | X) .: X = proj1 .: X by RELAT_1:129;
A5: proj1 .: X is real-bounded by A2, Th3;
then (proj1 | X) .: X is bounded_below by A4, XXREAL_2:def 11;
then A6: proj1 | X is bounded_below by A3, MEASURE6:def 10;
(proj1 | X) .: X is bounded_above by A4, A5, XXREAL_2:def 11;
then proj1 | X is bounded_above by A3, MEASURE6:def 11;
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:8;
A7: (proj1 | X) . p9 = p `1 by A1, PSCOMP_1:22;
then lower_bound f <= p `1 by PSCOMP_1:1;
hence ( lower_bound (proj1 | X) <= p `1 & p `1 <= upper_bound (proj1 | X) ) by A7, PSCOMP_1:4; :: thesis: verum