let p be Point of (TOP-REAL 2); for C being compact Subset of (TOP-REAL 2) st p in BDD C holds
(LSeg ((North-Bound (p,C)),(South-Bound (p,C)))) /\ C = {(North-Bound (p,C)),(South-Bound (p,C))}
let C be compact Subset of (TOP-REAL 2); ( p in BDD C implies (LSeg ((North-Bound (p,C)),(South-Bound (p,C)))) /\ C = {(North-Bound (p,C)),(South-Bound (p,C))} )
set L = LSeg ((North-Bound (p,C)),(South-Bound (p,C)));
assume A1:
p in BDD C
; (LSeg ((North-Bound (p,C)),(South-Bound (p,C)))) /\ C = {(North-Bound (p,C)),(South-Bound (p,C))}
then A2:
( North-Bound (p,C) in C & South-Bound (p,C) in C )
by Th17;
hereby TARSKI:def 3,
XBOOLE_0:def 10 {(North-Bound (p,C)),(South-Bound (p,C))} c= (LSeg ((North-Bound (p,C)),(South-Bound (p,C)))) /\ C
A3:
(North-Bound (p,C)) `2 = lower_bound (proj2 .: (C /\ (north_halfline p)))
by EUCLID:52;
A4:
(South-Bound (p,C)) `2 = upper_bound (proj2 .: (C /\ (south_halfline p)))
by EUCLID:52;
let x be
object ;
( x in (LSeg ((North-Bound (p,C)),(South-Bound (p,C)))) /\ C implies x in {(North-Bound (p,C)),(South-Bound (p,C))} )A5:
(South-Bound (p,C)) `1 = p `1
by EUCLID:52;
assume A6:
x in (LSeg ((North-Bound (p,C)),(South-Bound (p,C)))) /\ C
;
x in {(North-Bound (p,C)),(South-Bound (p,C))}then reconsider y =
x as
Point of
(TOP-REAL 2) ;
A7:
x in LSeg (
(North-Bound (p,C)),
(South-Bound (p,C)))
by A6, XBOOLE_0:def 4;
(
LSeg (
(North-Bound (p,C)),
(South-Bound (p,C))) is
vertical &
South-Bound (
p,
C)
in LSeg (
(North-Bound (p,C)),
(South-Bound (p,C))) )
by Th21, RLTOPSP1:68;
then A8:
y `1 = p `1
by A5, A7, SPPOL_1:def 3;
A9:
x in C
by A6, XBOOLE_0:def 4;
A10:
(North-Bound (p,C)) `1 = p `1
by EUCLID:52;
now ( y <> North-Bound (p,C) implies y = South-Bound (p,C) )
C /\ (north_halfline p) is
bounded
by TOPREAL6:89;
then
proj2 .: (C /\ (north_halfline p)) is
real-bounded
by JCT_MISC:14;
then A11:
proj2 .: (C /\ (north_halfline p)) is
bounded_below
;
(
(South-Bound (p,C)) `2 < p `2 &
p `2 < (North-Bound (p,C)) `2 )
by A1, Th18;
then A12:
(South-Bound (p,C)) `2 < (North-Bound (p,C)) `2
by XXREAL_0:2;
then A13:
(South-Bound (p,C)) `2 <= y `2
by A7, TOPREAL1:4;
assume
y <> North-Bound (
p,
C)
;
y = South-Bound (p,C)then A14:
y `2 <> (North-Bound (p,C)) `2
by A10, A8, TOPREAL3:6;
A15:
y `2 = proj2 . y
by PSCOMP_1:def 6;
y `2 <= (North-Bound (p,C)) `2
by A7, A12, TOPREAL1:4;
then A16:
y `2 < (North-Bound (p,C)) `2
by A14, XXREAL_0:1;
then
y in south_halfline p
by A8, TOPREAL1:def 12;
then
y in C /\ (south_halfline p)
by A9, XBOOLE_0:def 4;
then A17:
y `2 in proj2 .: (C /\ (south_halfline p))
by A15, FUNCT_2:35;
C /\ (south_halfline p) is
bounded
by TOPREAL6:89;
then
proj2 .: (C /\ (south_halfline p)) is
real-bounded
by JCT_MISC:14;
then
proj2 .: (C /\ (south_halfline p)) is
bounded_above
;
then
y `2 <= (South-Bound (p,C)) `2
by A4, A17, SEQ_4:def 1;
then
y `2 = (South-Bound (p,C)) `2
by A13, XXREAL_0:1;
hence
y = South-Bound (
p,
C)
by A5, A8, TOPREAL3:6;
verum end; hence
x in {(North-Bound (p,C)),(South-Bound (p,C))}
by TARSKI:def 2;
verum
end;
let x be object ; TARSKI:def 3 ( not x in {(North-Bound (p,C)),(South-Bound (p,C))} or x in (LSeg ((North-Bound (p,C)),(South-Bound (p,C)))) /\ C )
assume
x in {(North-Bound (p,C)),(South-Bound (p,C))}
; x in (LSeg ((North-Bound (p,C)),(South-Bound (p,C)))) /\ C
then A18:
( x = North-Bound (p,C) or x = South-Bound (p,C) )
by TARSKI:def 2;
then
x in LSeg ((North-Bound (p,C)),(South-Bound (p,C)))
by RLTOPSP1:68;
hence
x in (LSeg ((North-Bound (p,C)),(South-Bound (p,C)))) /\ C
by A18, A2, XBOOLE_0:def 4; verum