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