let p be Point of (TOP-REAL 2); 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); ( 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
; ( (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;
( 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;
( (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; 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; verum