let p, q be Point of (); :: thesis: for C being compact Subset of () 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 (); :: 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 /\ ())) & (South-Bound (q,C)) `2 = upper_bound (proj2 .: (C /\ ())) ) by EUCLID:52;
A3: ( (North-Bound (p,C)) `2 = lower_bound (proj2 .: (C /\ ())) & (South-Bound (p,C)) `2 = upper_bound (proj2 .: (C /\ ())) ) 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 ; :: according to ZFMISC_1:def 6 :: thesis: verum