let p be Point of (TOP-REAL 2); :: thesis: for C being compact Subset of (TOP-REAL 2) st p in BDD C holds

lower_bound (proj2 .: (C /\ (north_halfline p))) > upper_bound (proj2 .: (C /\ (south_halfline p)))

let C be compact Subset of (TOP-REAL 2); :: thesis: ( p in BDD C implies lower_bound (proj2 .: (C /\ (north_halfline p))) > upper_bound (proj2 .: (C /\ (south_halfline p))) )

assume p in BDD C ; :: thesis: lower_bound (proj2 .: (C /\ (north_halfline p))) > upper_bound (proj2 .: (C /\ (south_halfline p)))

then A1: ( (South-Bound (p,C)) `2 < p `2 & p `2 < (North-Bound (p,C)) `2 ) by Th18;

( (North-Bound (p,C)) `2 = lower_bound (proj2 .: (C /\ (north_halfline p))) & (South-Bound (p,C)) `2 = upper_bound (proj2 .: (C /\ (south_halfline p))) ) by EUCLID:52;

hence lower_bound (proj2 .: (C /\ (north_halfline p))) > upper_bound (proj2 .: (C /\ (south_halfline p))) by A1, XXREAL_0:2; :: thesis: verum

lower_bound (proj2 .: (C /\ (north_halfline p))) > upper_bound (proj2 .: (C /\ (south_halfline p)))

let C be compact Subset of (TOP-REAL 2); :: thesis: ( p in BDD C implies lower_bound (proj2 .: (C /\ (north_halfline p))) > upper_bound (proj2 .: (C /\ (south_halfline p))) )

assume p in BDD C ; :: thesis: lower_bound (proj2 .: (C /\ (north_halfline p))) > upper_bound (proj2 .: (C /\ (south_halfline p)))

then A1: ( (South-Bound (p,C)) `2 < p `2 & p `2 < (North-Bound (p,C)) `2 ) by Th18;

( (North-Bound (p,C)) `2 = lower_bound (proj2 .: (C /\ (north_halfline p))) & (South-Bound (p,C)) `2 = upper_bound (proj2 .: (C /\ (south_halfline p))) ) by EUCLID:52;

hence lower_bound (proj2 .: (C /\ (north_halfline p))) > upper_bound (proj2 .: (C /\ (south_halfline p))) by A1, XXREAL_0:2; :: thesis: verum