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:106;
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 Th17;
set EX = |[((p `1) - (r / 2)),(p `2)]|;
0 < r / 2 by A2, XREAL_1:139;
then (p `1) + (r / 2) > (p `1) + 0 by XREAL_1:6;
then A4: (p `1) - (r / 2) < p `1 by XREAL_1:19;
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, 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) - (r / 2)),(p `2)]| in Ball (P,r) by A2, A7, GOBOARD6:9;
hence contradiction by A3, A6; :: thesis: verum