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

( 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