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;

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;

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

( (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

( North-Bound (p,C) in C & North-Bound (p,C) in north_halfline p )
by A1, Th17;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;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

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

( (South-Bound (p,C)) `2 = upper_bound (proj2 .: (C /\ (south_halfline p))) & upper_bound (proj2 .: (south_halfline p)) = p `2 )
by Th8, EUCLID:52;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;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

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