let p be Point of (TOP-REAL 2); 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); ( 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:73;
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:23, JORDAN2C:16;
then A2:
proj2 .: (C /\ (north_halfline p)) is bounded_below
by XXREAL_2:def 11;
assume A3:
p in BDD C
; ( 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:137;
then A4:
not C /\ (north_halfline p) is empty
by XBOOLE_0:def 7;
C /\ (north_halfline p) is Bounded
by A1, JORDAN2C:16, XBOOLE_1:17;
then
proj2 .: (C /\ (north_halfline p)) is closed
by JCT_MISC:22;
then
inf (proj2 .: (C /\ (north_halfline p))) in proj2 .: (C /\ (north_halfline p))
by A4, A2, Lm2, RCOMP_1:31, RELAT_1:152;
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:
inf (proj2 .: (C /\ (north_halfline p))) = proj2 . x
by FUNCT_2:115;
reconsider x = x as Point of (TOP-REAL 2) by A5;
A8: x `2 =
inf (proj2 .: (C /\ (north_halfline p)))
by A7, PSCOMP_1:def 29
.=
(North-Bound p,C) `2
by EUCLID:56
;
x in north_halfline p
by A6, XBOOLE_0:def 4;
then x `1 =
p `1
by TOPREAL1:def 12
.=
(North-Bound p,C) `1
by EUCLID:56
;
then
x = North-Bound p,C
by A8, TOPREAL3:11;
hence
( North-Bound p,C in C & North-Bound p,C in north_halfline p )
by A6, XBOOLE_0:def 4; ( 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:23, JORDAN2C:16;
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:136;
then A10:
not C /\ (south_halfline p) is empty
by XBOOLE_0:def 7;
C /\ (south_halfline p) is Bounded
by A1, JORDAN2C:16, XBOOLE_1:17;
then
proj2 .: (C /\ (south_halfline p)) is closed
by JCT_MISC:22;
then
sup (proj2 .: (C /\ (south_halfline p))) in proj2 .: (C /\ (south_halfline p))
by A10, A9, Lm2, RCOMP_1:30, RELAT_1:152;
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:
sup (proj2 .: (C /\ (south_halfline p))) = proj2 . x
by FUNCT_2:115;
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 14
.=
(South-Bound p,C) `1
by EUCLID:56
;
x `2 =
sup (proj2 .: (C /\ (south_halfline p)))
by A13, PSCOMP_1:def 29
.=
(South-Bound p,C) `2
by EUCLID:56
;
then
x = South-Bound p,C
by A14, TOPREAL3:11;
hence
( South-Bound p,C in C & South-Bound p,C in south_halfline p )
by A12, XBOOLE_0:def 4; verum