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) <> North-Bound (p,C)

let C be compact Subset of (TOP-REAL 2); :: thesis: ( p in BDD C implies South-Bound (p,C) <> North-Bound (p,C) )

assume A1: p in BDD C ; :: thesis: South-Bound (p,C) <> North-Bound (p,C)

A2: ( (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;

assume not South-Bound (p,C) <> North-Bound (p,C) ; :: thesis: contradiction

hence contradiction by A1, A2, Th19; :: thesis: verum

South-Bound (p,C) <> North-Bound (p,C)

let C be compact Subset of (TOP-REAL 2); :: thesis: ( p in BDD C implies South-Bound (p,C) <> North-Bound (p,C) )

assume A1: p in BDD C ; :: thesis: South-Bound (p,C) <> North-Bound (p,C)

A2: ( (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;

assume not South-Bound (p,C) <> North-Bound (p,C) ; :: thesis: contradiction

hence contradiction by A1, A2, Th19; :: thesis: verum