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

let C be compact Subset of (); :: thesis: ( p in BDD C implies ( North-Bound (p,C) in C & North-Bound (p,C) in north_halfline p & South-Bound (p,C) in C & South-Bound (p,C) in south_halfline p ) )
set X = C /\ ();
C /\ () c= C by XBOOLE_1:17;
then proj2 .: (C /\ ()) is real-bounded by ;
then A1: proj2 .: (C /\ ()) is bounded_below ;
assume A2: p in BDD C ; :: thesis: ( North-Bound (p,C) in C & North-Bound (p,C) in north_halfline p & South-Bound (p,C) in C & South-Bound (p,C) in south_halfline p )
then not north_halfline p c= UBD C by Th11;
then north_halfline p meets C by JORDAN2C:129;
then A3: not C /\ () is empty ;
C /\ () is bounded by ;
then proj2 .: (C /\ ()) is closed by JCT_MISC:13;
then lower_bound (proj2 .: (C /\ ())) in proj2 .: (C /\ ()) by ;
then consider x being object such that
A4: x in the carrier of () and
A5: x in C /\ () and
A6: lower_bound (proj2 .: (C /\ ())) = proj2 . x by FUNCT_2:64;
reconsider x = x as Point of () by A4;
A7: x `2 = lower_bound (proj2 .: (C /\ ())) by
.= (North-Bound (p,C)) `2 by EUCLID:52 ;
x in north_halfline p by ;
then x `1 = p `1 by TOPREAL1:def 10
.= (North-Bound (p,C)) `1 by EUCLID:52 ;
then x = North-Bound (p,C) by ;
hence ( North-Bound (p,C) in C & North-Bound (p,C) in north_halfline p ) by ; :: thesis: ( South-Bound (p,C) in C & South-Bound (p,C) in south_halfline p )
set X = C /\ ();
C /\ () c= C by XBOOLE_1:17;
then proj2 .: (C /\ ()) is real-bounded by ;
then A8: proj2 .: (C /\ ()) is bounded_above ;
not south_halfline p c= UBD C by ;
then south_halfline p meets C by JORDAN2C:128;
then A9: not C /\ () is empty ;
C /\ () is bounded by ;
then proj2 .: (C /\ ()) is closed by JCT_MISC:13;
then upper_bound (proj2 .: (C /\ ())) in proj2 .: (C /\ ()) by ;
then consider x being object such that
A10: x in the carrier of () and
A11: x in C /\ () and
A12: upper_bound (proj2 .: (C /\ ())) = proj2 . x by FUNCT_2:64;
reconsider x = x as Point of () by A10;
x in south_halfline p by ;
then A13: x `1 = p `1 by TOPREAL1:def 12
.= (South-Bound (p,C)) `1 by EUCLID:52 ;
x `2 = upper_bound (proj2 .: (C /\ ())) by
.= (South-Bound (p,C)) `2 by EUCLID:52 ;
then x = South-Bound (p,C) by ;
hence ( South-Bound (p,C) in C & South-Bound (p,C) in south_halfline p ) by ; :: thesis: verum