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 )
then ( South-Bound p,C in C & South-Bound p,C in south_halfline p ) by Th22;
then South-Bound p,C in C /\ (south_halfline p) by XBOOLE_0:def 4;
then A2: not proj2 .: (C /\ (south_halfline p)) is empty by Lm2, RELAT_1:152;
A3: BDD C misses C by JORDAN1A:15;

A4: now

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

end;

( 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 A6: not proj2 .: (C /\ (north_halfline p)) is empty by Lm2, RELAT_1:152;
( proj2 .: (south_halfline p) is bounded_above & C /\ (south_halfline p) c= south_halfline p ) by Th5, XBOOLE_1:17;
then A7: sup (proj2 .: (C /\ (south_halfline p))) <= sup (proj2 .: (south_halfline p)) by A2, RELAT_1:156, SEQ_4:65;

A8: now

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

end;

( (South-Bound p,C) `2 = sup (proj2 .: (C /\ (south_halfline p))) & sup (proj2 .: (south_halfline p)) = p `2 ) by Th9, EUCLID:56;
hence (South-Bound p,C) `2 < p `2 by A7, A4, XXREAL_0:1; :: thesis: p `2 < (North-Bound p,C) `2
( proj2 .: (north_halfline p) is bounded_below & C /\ (north_halfline p) c= north_halfline p ) by Th4, XBOOLE_1:17;
then A10: inf (proj2 .: (C /\ (north_halfline p))) >= inf (proj2 .: (north_halfline p)) by A6, RELAT_1:156, SEQ_4:64;
( inf (proj2 .: (north_halfline p)) = p `2 & (North-Bound p,C) `2 = inf (proj2 .: (C /\ (north_halfline p))) ) by Th8, EUCLID:56;
hence p `2 < (North-Bound p,C) `2 by A10, A8, XXREAL_0:1; :: thesis: verum