let p be Point of (TOP-REAL 2); for C being compact Subset of (TOP-REAL 2) st p in BDD C holds
p `1 <> E-bound (BDD C)
reconsider P = p as Point of (Euclid 2) by Lm3;
let C be compact Subset of (TOP-REAL 2); ( p in BDD C implies p `1 <> E-bound (BDD C) )
A1:
BDD C is bounded
by JORDAN2C:106;
assume
p in BDD C
; p `1 <> E-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 A4:
(p `1) + (r / 2) > (p `1) + 0
by XREAL_1:6;
assume A5:
p `1 = E-bound (BDD C)
; contradiction
A6:
not |[((p `1) + (r / 2)),(p `2)]| in BDD C
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:7;
hence
contradiction
by A3, A6; verum