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 ) )
A1: C is Bounded by JORDAN2C:65;
set X = C /\ (north_halfline p);
C /\ (north_halfline p) c= C by XBOOLE_1:17;
then proj2 .: (C /\ (north_halfline p)) is bounded by A1, JCT_MISC:14, JORDAN2C:12;
then A2: proj2 .: (C /\ (north_halfline p)) is bounded_below by XXREAL_2:def 11;
assume A3: 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 Th12;
then north_halfline p meets C by JORDAN2C:129;
then A4: not C /\ (north_halfline p) is empty by XBOOLE_0:def 7;
C /\ (north_halfline p) is Bounded by A1, JORDAN2C:12, XBOOLE_1:17;
then proj2 .: (C /\ (north_halfline p)) is closed by JCT_MISC:13;
then lower_bound (proj2 .: (C /\ (north_halfline p))) in proj2 .: (C /\ (north_halfline p)) by A4, A2, Lm2, RCOMP_1:13, RELAT_1:119;
then consider x being set such that
A5: x in the carrier of (TOP-REAL 2) and
A6: x in C /\ (north_halfline p) and
A7: lower_bound (proj2 .: (C /\ (north_halfline p))) = proj2 . x by FUNCT_2:64;
reconsider x = x as Point of (TOP-REAL 2) by A5;
A8: x `2 = lower_bound (proj2 .: (C /\ (north_halfline p))) by A7, PSCOMP_1:def 6
.= (North-Bound (p,C)) `2 by EUCLID:52 ;
x in north_halfline p by A6, XBOOLE_0:def 4;
then x `1 = p `1 by TOPREAL1:def 10
.= (North-Bound (p,C)) `1 by EUCLID:52 ;
then x = North-Bound (p,C) by A8, TOPREAL3:6;
hence ( North-Bound (p,C) in C & North-Bound (p,C) in north_halfline p ) by A6, 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);
C /\ (south_halfline p) c= C by XBOOLE_1:17;
then proj2 .: (C /\ (south_halfline p)) is bounded by A1, JCT_MISC:14, JORDAN2C:12;
then A9: proj2 .: (C /\ (south_halfline p)) is bounded_above by XXREAL_2:def 11;
not south_halfline p c= UBD C by A3, Th13;
then south_halfline p meets C by JORDAN2C:128;
then A10: not C /\ (south_halfline p) is empty by XBOOLE_0:def 7;
C /\ (south_halfline p) is Bounded by A1, JORDAN2C:12, XBOOLE_1:17;
then proj2 .: (C /\ (south_halfline p)) is closed by JCT_MISC:13;
then upper_bound (proj2 .: (C /\ (south_halfline p))) in proj2 .: (C /\ (south_halfline p)) by A10, A9, Lm2, RCOMP_1:12, RELAT_1:119;
then consider x being set such that
A11: x in the carrier of (TOP-REAL 2) and
A12: x in C /\ (south_halfline p) and
A13: upper_bound (proj2 .: (C /\ (south_halfline p))) = proj2 . x by FUNCT_2:64;
reconsider x = x as Point of (TOP-REAL 2) by A11;
x in south_halfline p by A12, XBOOLE_0:def 4;
then A14: x `1 = p `1 by TOPREAL1:def 12
.= (South-Bound (p,C)) `1 by EUCLID:52 ;
x `2 = upper_bound (proj2 .: (C /\ (south_halfline p))) by A13, PSCOMP_1:def 6
.= (South-Bound (p,C)) `2 by EUCLID:52 ;
then x = South-Bound (p,C) by A14, TOPREAL3:6;
hence ( South-Bound (p,C) in C & South-Bound (p,C) in south_halfline p ) by A12, XBOOLE_0:def 4; :: thesis: verum