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 Th17;
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:119;
A3: BDD C misses C by JORDAN1A:7;

A4: now :: thesis: not (South-Bound (p,C)) `2 = p `2

A5: (South-Bound (p,C)) `1 = p `1 by EUCLID:52;
assume (South-Bound (p,C)) `2 = p `2 ; :: thesis: contradiction
then South-Bound (p,C) = p by A5, TOPREAL3:6;
then p in C by A1, Th17;
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, Th17;
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:119;
( proj2 .: (south_halfline p) is bounded_above & C /\ (south_halfline p) c= south_halfline p ) by Th4, XBOOLE_1:17;
then A7: upper_bound (proj2 .: (C /\ (south_halfline p))) <= upper_bound (proj2 .: (south_halfline p)) by A2, RELAT_1:123, SEQ_4:48;

A8: now :: thesis: not (North-Bound (p,C)) `2 = p `2

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

end;

( (South-Bound (p,C)) `2 = upper_bound (proj2 .: (C /\ (south_halfline p))) & upper_bound (proj2 .: (south_halfline p)) = p `2 ) by Th8, EUCLID:52;
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 Th3, XBOOLE_1:17;
then A10: lower_bound (proj2 .: (C /\ (north_halfline p))) >= lower_bound (proj2 .: (north_halfline p)) by A6, RELAT_1:123, SEQ_4:47;
( lower_bound (proj2 .: (north_halfline p)) = p `2 & (North-Bound (p,C)) `2 = lower_bound (proj2 .: (C /\ (north_halfline p))) ) by Th7, EUCLID:52;
hence p `2 < (North-Bound (p,C)) `2 by A10, A8, XXREAL_0:1; :: thesis: verum