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 <> S-bound (BDD C)
let C be compact Subset of (TOP-REAL 2); :: thesis: ( p in BDD C implies p `2 <> S-bound (BDD C) )
assume A1: p in BDD C ; :: thesis: p `2 <> S-bound (BDD C)
reconsider P = p as Point of (Euclid 2) by Lm3;
consider r being Real such that
A2: ( r > 0 & Ball P,r c= BDD C ) by A1, Th29;
assume A3: p `2 = S-bound (BDD C) ; :: thesis: contradiction
A4: BDD C is Bounded by JORDAN2C:114;
A5: 0 < r / 2 by A2, XREAL_1:141;
A6: r / 2 < r by A2, XREAL_1:218;
(p `2 ) + (r / 2) > (p `2 ) + 0 by A5, XREAL_1:8;
then A7: (p `2 ) - (r / 2) < p `2 by XREAL_1:21;
set EX = |[(p `1 ),((p `2 ) - (r / 2))]|;
P = |[(p `1 ),(p `2 )]| by EUCLID:57;
then A8: |[(p `1 ),((p `2 ) - (r / 2))]| in Ball P,r by A2, A6, GOBOARD6:13;
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 >= S-bound (BDD C) by A4, Th6;
hence contradiction by A3, A7, EUCLID:56; :: thesis: verum

end;

hence contradiction by A2, A8; :: thesis: verum