let p be Point of ; :: thesis: for C being compact Subset of st p in BDD C holds
South-Bound p,C <> North-Bound p,C
let C be compact Subset of ; :: 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 = inf (proj2 .: (C /\ (north_halfline p))) & (South-Bound p,C) `2 = sup (proj2 .: (C /\ (south_halfline p))) ) by EUCLID:56;
assume not South-Bound p,C <> North-Bound p,C ; :: thesis: contradiction
hence contradiction by A1, A2, Th24; :: thesis: verum