let p be Point of (TOP-REAL 2); :: thesis: for C being compact Subset of (TOP-REAL 2) st p in BDD C holds
p `2 <> N-bound (BDD C)
reconsider P = p as Point of (Euclid 2) by Lm3;
let C be compact Subset of (TOP-REAL 2); :: thesis: ( p in BDD C implies p `2 <> N-bound (BDD C) )
A1: BDD C is bounded by JORDAN2C:106;
assume p in BDD C ; :: thesis: p `2 <> N-bound (BDD C)
then consider r being Real such that
A2: r > 0 and
A3: Ball (P,r) c= BDD C by Th17;
set EX = |[(p `1),((p `2) + (r / 2))]|;
0 < r / 2 by A2, XREAL_1:139;
then A4: (p `2) + (r / 2) > (p `2) + 0 by XREAL_1:6;
assume A5: p `2 = N-bound (BDD C) ; :: thesis: contradiction
A6: not |[(p `1),((p `2) + (r / 2))]| in BDD C

proof

assume |[(p `1),((p `2) + (r / 2))]| in BDD C ; :: thesis: contradiction
then |[(p `1),((p `2) + (r / 2))]| `2 <= N-bound (BDD C) by A1, Th5;
hence contradiction by A5, A4, EUCLID:52; :: thesis: verum

end;

A7: P = |[(p `1),(p `2)]| by EUCLID:53;
r / 2 < r by A2, XREAL_1:216;
then |[(p `1),((p `2) + (r / 2))]| in Ball (P,r) by A2, A7, GOBOARD6:8;
hence contradiction by A3, A6; :: thesis: verum