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:114;
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 Th29;
set EX = |[(p `1 ),((p `2 ) + (r / 2))]|;
0 < r / 2 by A2, XREAL_1:141;
then A4: (p `2 ) + (r / 2) > (p `2 ) + 0 by XREAL_1:8;
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, Th6;
hence contradiction by A5, A4, EUCLID:56; :: thesis: verum

end;

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