let p be Point of (TOP-REAL 2); :: thesis: for C being compact Subset of (TOP-REAL 2) 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 (TOP-REAL 2); :: 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 ) )
assume A1: 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 )
A2: C is Bounded by JORDAN2C:73;
set X = C /\ (north_halfline p);
not north_halfline p c= UBD C by A1, Th12;
then north_halfline p meets C by JORDAN2C:137;
then A3: not C /\ (north_halfline p) is empty by XBOOLE_0:def 7;
A4: C /\ (north_halfline p) c= C by XBOOLE_1:17;
A5: C /\ (north_halfline p) is Bounded by A2, JORDAN2C:16, XBOOLE_1:17;
C /\ (north_halfline p) is closed by TOPS_1:35;
then A6: proj2 .: (C /\ (north_halfline p)) is closed by A5, JCT_MISC:22;
proj2 .: (C /\ (north_halfline p)) is bounded by A2, A4, JCT_MISC:23, JORDAN2C:16;
then proj2 .: (C /\ (north_halfline p)) is bounded_below by XXREAL_2:def 11;
then inf (proj2 .: (C /\ (north_halfline p))) in proj2 .: (C /\ (north_halfline p)) by A3, A6, Lm2, RCOMP_1:31, RELAT_1:152;
then consider x being set such that
A7: x in the carrier of (TOP-REAL 2) and
A8: x in C /\ (north_halfline p) and
A9: inf (proj2 .: (C /\ (north_halfline p))) = proj2 . x by FUNCT_2:115;
reconsider x = x as Point of (TOP-REAL 2) by A7;
x in north_halfline p by A8, XBOOLE_0:def 4;
then A10: x `1 = p `1 by TOPREAL1:def 12
.= (North-Bound p,C) `1 by EUCLID:56 ;
x `2 = inf (proj2 .: (C /\ (north_halfline p))) by A9, PSCOMP_1:def 29
.= (North-Bound p,C) `2 by EUCLID:56 ;
then x = North-Bound p,C by A10, TOPREAL3:11;
hence ( North-Bound p,C in C & North-Bound p,C in north_halfline p ) by A8, XBOOLE_0:def 4; :: thesis: ( South-Bound p,C in C & South-Bound p,C in south_halfline p )
set X = C /\ (south_halfline p);
not south_halfline p c= UBD C by A1, Th13;
then south_halfline p meets C by JORDAN2C:136;
then A11: not C /\ (south_halfline p) is empty by XBOOLE_0:def 7;
A12: C /\ (south_halfline p) c= C by XBOOLE_1:17;
A13: C /\ (south_halfline p) is Bounded by A2, JORDAN2C:16, XBOOLE_1:17;
C /\ (south_halfline p) is closed by TOPS_1:35;
then A14: proj2 .: (C /\ (south_halfline p)) is closed by A13, JCT_MISC:22;
proj2 .: (C /\ (south_halfline p)) is bounded by A2, A12, JCT_MISC:23, JORDAN2C:16;
then proj2 .: (C /\ (south_halfline p)) is bounded_above by XXREAL_2:def 11;
then sup (proj2 .: (C /\ (south_halfline p))) in proj2 .: (C /\ (south_halfline p)) by A11, A14, Lm2, RCOMP_1:30, RELAT_1:152;
then consider x being set such that
A15: x in the carrier of (TOP-REAL 2) and
A16: x in C /\ (south_halfline p) and
A17: sup (proj2 .: (C /\ (south_halfline p))) = proj2 . x by FUNCT_2:115;
reconsider x = x as Point of (TOP-REAL 2) by A15;
x in south_halfline p by A16, XBOOLE_0:def 4;
then A18: x `1 = p `1 by TOPREAL1:def 14
.= (South-Bound p,C) `1 by EUCLID:56 ;
x `2 = sup (proj2 .: (C /\ (south_halfline p))) by A17, PSCOMP_1:def 29
.= (South-Bound p,C) `2 by EUCLID:56 ;
then x = South-Bound p,C by A18, TOPREAL3:11;
hence ( South-Bound p,C in C & South-Bound p,C in south_halfline p ) by A16, XBOOLE_0:def 4; :: thesis: verum