let p be Point of (); :: thesis: for C being compact Subset of () st p in BDD C holds
( (South-Bound (p,C)) `2 < p `2 & p `2 < (North-Bound (p,C)) `2 )

let C be compact Subset of (); :: thesis: ( p in BDD C implies ( (South-Bound (p,C)) `2 < p `2 & p `2 < (North-Bound (p,C)) `2 ) )
assume A1: p in BDD C ; :: thesis: ( (South-Bound (p,C)) `2 < p `2 & p `2 < (North-Bound (p,C)) `2 )
then ( South-Bound (p,C) in C & South-Bound (p,C) in south_halfline p ) by Th17;
then South-Bound (p,C) in C /\ () by XBOOLE_0:def 4;
then A2: not proj2 .: (C /\ ()) is empty by ;
A3: BDD C misses C by JORDAN1A:7;
A4: now :: thesis: not (South-Bound (p,C)) `2 = p `2
A5: (South-Bound (p,C)) `1 = p `1 by EUCLID:52;
assume (South-Bound (p,C)) `2 = p `2 ; :: thesis: contradiction
then South-Bound (p,C) = p by ;
then p in C by ;
hence contradiction by A1, A3, XBOOLE_0:3; :: thesis: verum
end;
( North-Bound (p,C) in C & North-Bound (p,C) in north_halfline p ) by ;
then not C /\ () is empty by XBOOLE_0:def 4;
then A6: not proj2 .: (C /\ ()) is empty by ;
( proj2 .: () is bounded_above & C /\ () c= south_halfline p ) by ;
then A7: upper_bound (proj2 .: (C /\ ())) <= upper_bound () by ;
A8: now :: thesis: not (North-Bound (p,C)) `2 = p `2
A9: (North-Bound (p,C)) `1 = p `1 by EUCLID:52;
assume (North-Bound (p,C)) `2 = p `2 ; :: thesis: contradiction
then North-Bound (p,C) = p by ;
then p in C by ;
hence contradiction by A1, A3, XBOOLE_0:3; :: thesis: verum
end;
( (South-Bound (p,C)) `2 = upper_bound (proj2 .: (C /\ ())) & upper_bound () = p `2 ) by ;
hence (South-Bound (p,C)) `2 < p `2 by ; :: thesis: p `2 < (North-Bound (p,C)) `2
( proj2 .: () is bounded_below & C /\ () c= north_halfline p ) by ;
then A10: lower_bound (proj2 .: (C /\ ())) >= lower_bound () by ;
( lower_bound () = p `2 & (North-Bound (p,C)) `2 = lower_bound (proj2 .: (C /\ ())) ) by ;
hence p `2 < (North-Bound (p,C)) `2 by ; :: thesis: verum