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 `1 <> W-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 `1 <> W-bound (BDD C) )
A1: BDD C is Bounded by JORDAN2C:114;
assume p in BDD C ; :: thesis: p `1 <> W-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 ) - (r / 2)),(p `2 )]|;
0 < r / 2 by A2, XREAL_1:141;
then (p `1 ) + (r / 2) > (p `1 ) + 0 by XREAL_1:8;
then A4: (p `1 ) - (r / 2) < p `1 by XREAL_1:21;
assume A5: p `1 = W-bound (BDD C) ; :: thesis: contradiction
A6: not |[((p `1 ) - (r / 2)),(p `2 )]| in BDD C

proof

assume |[((p `1 ) - (r / 2)),(p `2 )]| in BDD C ; :: thesis: contradiction
then |[((p `1 ) - (r / 2)),(p `2 )]| `1 >= W-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 ) - (r / 2)),(p `2 )]| in Ball P,r by A2, A7, GOBOARD6:12;
hence contradiction by A3, A6; :: thesis: verum