let C be Subset of (TOP-REAL 2); :: thesis: ( C is Bounded implies for h being real number st BDD C <> {} & h > W-bound (BDD C) holds
ex p being Point of (TOP-REAL 2) st
( p in BDD C & not p `1 >= h ) )
assume A1: C is Bounded ; :: thesis: for h being real number st BDD C <> {} & h > W-bound (BDD C) holds
ex p being Point of (TOP-REAL 2) st
( p in BDD C & not p `1 >= h )
set X = proj1 | (BDD C);
let h be real number ; :: thesis: ( BDD C <> {} & h > W-bound (BDD C) implies ex p being Point of (TOP-REAL 2) st
( p in BDD C & not p `1 >= h ) )
assume that
A2: BDD C <> {} and
A3: h > W-bound (BDD C) and
A4: for p being Point of (TOP-REAL 2) st p in BDD C holds
p `1 >= h ; :: thesis: contradiction
reconsider T = (TOP-REAL 2) | (BDD C) as non empty TopSpace by A2;
the carrier of T = BDD C by PRE_TOPC:29;
then (proj1 | (BDD C)) .: the carrier of T = proj1 .: (BDD C) by RELAT_1:162;
then (proj1 | (BDD C)) .: the carrier of T is bounded by A1, Th4, JORDAN2C:114;
then (proj1 | (BDD C)) .: the carrier of T is bounded_below by XXREAL_2:def 11;
then reconsider X = proj1 | (BDD C) as bounded_below RealMap of T by MEASURE6:def 14;
A5: for p being Point of T holds X . p >= h

proof

let p be Point of T; :: thesis: X . p >= h
A6: the carrier of T = BDD C by PRE_TOPC:29;
then p in BDD C ;
then reconsider p9 = p as Point of (TOP-REAL 2) ;
X . p = proj1 . p9 by A6, FUNCT_1:72;
then X . p = p9 `1 by PSCOMP_1:def 28;
hence X . p >= h by A4, A6; :: thesis: verum

end;

A7: h is Real by XREAL_0:def 1;
lower_bound X = W-bound (BDD C) by PSCOMP_1:def 30;
hence contradiction by A3, A7, A5, PSCOMP_1:48; :: thesis: verum