let p, q be Point of (TOP-REAL 2); :: thesis: for C being compact Subset of (TOP-REAL 2) st p in BDD C & q in BDD C & p `1 <> q `1 holds
North-Bound p,C, South-Bound q,C, North-Bound q,C, South-Bound p,C are_mutually_different
let C be compact Subset of (TOP-REAL 2); :: thesis: ( p in BDD C & q in BDD C & p `1 <> q `1 implies North-Bound p,C, South-Bound q,C, North-Bound q,C, South-Bound p,C are_mutually_different )
assume that
A1: p in BDD C and
A2: q in BDD C and
A3: p `1 <> q `1 ; :: thesis: North-Bound p,C, South-Bound q,C, North-Bound q,C, South-Bound p,C are_mutually_different
set np = North-Bound p,C;
set sq = South-Bound q,C;
set nq = North-Bound q,C;
set sp = South-Bound p,C;
A4: ( (North-Bound p,C) `1 = p `1 & (North-Bound q,C) `1 = q `1 & (South-Bound p,C) `1 = p `1 & (South-Bound q,C) `1 = q `1 ) by EUCLID:56;
( (North-Bound q,C) `2 = inf (proj2 .: (C /\ (north_halfline q))) & (South-Bound q,C) `2 = sup (proj2 .: (C /\ (south_halfline q))) & (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;
hence ( North-Bound p,C <> South-Bound q,C & North-Bound p,C <> North-Bound q,C & North-Bound p,C <> South-Bound p,C & South-Bound q,C <> North-Bound q,C & South-Bound q,C <> South-Bound p,C & North-Bound q,C <> South-Bound p,C ) by A1, A2, A3, A4, Th24; :: according to ZFMISC_1:def 6 :: thesis: verum