let p be Point of (TOP-REAL 2); :: thesis: for C being compact Subset of (TOP-REAL 2) st p in BDD C holds
( (South-Bound p,C) `2 < p `2 & p `2 < (North-Bound p,C) `2 )
let C be compact Subset of (TOP-REAL 2); :: thesis: ( p in BDD C implies ( (South-Bound p,C) `2 < p `2 & p `2 < (North-Bound p,C) `2 ) )
assume A1: p in BDD C ; :: thesis: ( (South-Bound p,C) `2 < p `2 & p `2 < (North-Bound p,C) `2 )
A2: (South-Bound p,C) `2 = sup (proj2 .: (C /\ (south_halfline p))) by EUCLID:56;
A3: South-Bound p,C in C by A1, Th22;
South-Bound p,C in south_halfline p by A1, Th22;
then South-Bound p,C in C /\ (south_halfline p) by A3, XBOOLE_0:def 4;
then A4: not proj2 .: (C /\ (south_halfline p)) is empty by Lm2, RELAT_1:152;
A5: proj2 .: (south_halfline p) is bounded_above by Th5;
C /\ (south_halfline p) c= south_halfline p by XBOOLE_1:17;
then A6: sup (proj2 .: (C /\ (south_halfline p))) <= sup (proj2 .: (south_halfline p)) by A4, A5, RELAT_1:156, SEQ_4:65;
A7: sup (proj2 .: (south_halfline p)) = p `2 by Th9;
A8: BDD C misses C by JORDAN1A:15;

now

assume A9: (South-Bound p,C) `2 = p `2 ; :: thesis: contradiction
(South-Bound p,C) `1 = p `1 by EUCLID:56;
then South-Bound p,C = p by A9, TOPREAL3:11;
then p in C by A1, Th22;
hence contradiction by A1, A8, XBOOLE_0:3; :: thesis: verum

end;

hence (South-Bound p,C) `2 < p `2 by A2, A6, A7, XXREAL_0:1; :: thesis: p `2 < (North-Bound p,C) `2
( North-Bound p,C in C & North-Bound p,C in north_halfline p ) by A1, Th22;
then not C /\ (north_halfline p) is empty by XBOOLE_0:def 4;
then A10: not proj2 .: (C /\ (north_halfline p)) is empty by Lm2, RELAT_1:152;
A11: proj2 .: (north_halfline p) is bounded_below by Th4;
C /\ (north_halfline p) c= north_halfline p by XBOOLE_1:17;
then A12: inf (proj2 .: (C /\ (north_halfline p))) >= inf (proj2 .: (north_halfline p)) by A10, A11, RELAT_1:156, SEQ_4:64;
A13: inf (proj2 .: (north_halfline p)) = p `2 by Th8;
A14: (North-Bound p,C) `2 = inf (proj2 .: (C /\ (north_halfline p))) by EUCLID:56;

now

assume A15: (North-Bound p,C) `2 = p `2 ; :: thesis: contradiction
(North-Bound p,C) `1 = p `1 by EUCLID:56;
then North-Bound p,C = p by A15, TOPREAL3:11;
then p in C by A1, Th22;
hence contradiction by A1, A8, XBOOLE_0:3; :: thesis: verum

end;

hence p `2 < (North-Bound p,C) `2 by A12, A13, A14, XXREAL_0:1; :: thesis: verum