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_distinct
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_distinct )
set np = North-Bound (p,C);
set sq = South-Bound (q,C);
set nq = North-Bound (q,C);
set sp = South-Bound (p,C);
A1: ( (North-Bound (p,C)) `1 = p `1 & (South-Bound (p,C)) `1 = p `1 ) by EUCLID:52;
A2: ( (North-Bound (q,C)) `2 = lower_bound (proj2 .: (C /\ (north_halfline q))) & (South-Bound (q,C)) `2 = upper_bound (proj2 .: (C /\ (south_halfline q))) ) by EUCLID:52;
A3: ( (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 ( p in BDD C & q in BDD C & p `1 <> q `1 ) ; :: thesis: North-Bound (p,C), South-Bound (q,C), North-Bound (q,C), South-Bound (p,C) are_mutually_distinct
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, Th19, EUCLID:52; :: according to ZFMISC_1:def 6 :: thesis: verum