let C be Subset of (TOP-REAL 2); :: thesis: ( C is bounded implies for h being Real st BDD C <> {} & h < N-bound (BDD C) holds
ex p being Point of (TOP-REAL 2) st
( p in BDD C & not p `2 <= h ) )
assume A1: C is bounded ; :: thesis: for h being Real st BDD C <> {} & h < N-bound (BDD C) holds
ex p being Point of (TOP-REAL 2) st
( p in BDD C & not p `2 <= h )
set X = proj2 | (BDD C);
let h be Real; :: thesis: ( BDD C <> {} & h < N-bound (BDD C) implies ex p being Point of (TOP-REAL 2) st
( p in BDD C & not p `2 <= h ) )
assume that
A2: BDD C <> {} and
A3: h < N-bound (BDD C) and
A4: for p being Point of (TOP-REAL 2) st p in BDD C holds
p `2 <= 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:8;
then (proj2 | (BDD C)) .: the carrier of T = proj2 .: (BDD C) by RELAT_1:129;
then (proj2 | (BDD C)) .: the carrier of T is real-bounded by A1, JCT_MISC:14, JORDAN2C:106;
then (proj2 | (BDD C)) .: the carrier of T is bounded_above by XXREAL_2:def 11;
then reconsider X = proj2 | (BDD C) as bounded_above RealMap of T by MEASURE6:def 11;
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:8;
then p in BDD C ;
then reconsider p9 = p as Point of (TOP-REAL 2) ;
X . p = proj2 . p9 by A6, FUNCT_1:49;
then X . p = p9 `2 by PSCOMP_1:def 6;
hence X . p <= h by A4, A6; :: thesis: verum
end;
upper_bound X = N-bound (BDD C) by PSCOMP_1:def 8;
hence contradiction by A3, A5, PSCOMP_1:5; :: thesis: verum