let p be Point of (TOP-REAL 2); :: thesis: 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); :: thesis: ( 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 ; :: thesis: (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 Th22;

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: {(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:56;
A4: (South-Bound (p,C)) `2 = upper_bound (proj2 .: (C /\ (south_halfline p))) by EUCLID:56;
let x be set ; :: thesis: ( 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:56;
assume A6: x in (LSeg ((North-Bound (p,C)),(South-Bound (p,C)))) /\ C ; :: thesis: 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 Th26, RLTOPSP1:69;
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:56;

now

A11: C is Bounded by JORDAN2C:73;
then C /\ (north_halfline p) is Bounded by TOPREAL6:98;
then proj2 .: (C /\ (north_halfline p)) is bounded by JCT_MISC:23;
then A12: proj2 .: (C /\ (north_halfline p)) is bounded_below by XXREAL_2:def 11;
( (South-Bound (p,C)) `2 < p `2 & p `2 < (North-Bound (p,C)) `2 ) by A1, Th23;
then A13: (South-Bound (p,C)) `2 < (North-Bound (p,C)) `2 by XXREAL_0:2;
then A14: (South-Bound (p,C)) `2 <= y `2 by A7, TOPREAL1:10;
assume y <> North-Bound (p,C) ; :: thesis: y = South-Bound (p,C)
then A15: y `2 <> (North-Bound (p,C)) `2 by A10, A8, TOPREAL3:11;
A16: y `2 = proj2 . y by PSCOMP_1:def 29;
y `2 <= (North-Bound (p,C)) `2 by A7, A13, TOPREAL1:10;
then A17: y `2 < (North-Bound (p,C)) `2 by A15, XXREAL_0:1;

now

assume y `2 > p `2 ; :: thesis: contradiction
then y in north_halfline p by A8, TOPREAL1:def 12;
then y in C /\ (north_halfline p) by A9, XBOOLE_0:def 4;
then y `2 in proj2 .: (C /\ (north_halfline p)) by A16, FUNCT_2:43;
hence contradiction by A3, A17, A12, SEQ_4:def 5; :: thesis: verum

end;

then y in south_halfline p by A8, TOPREAL1:def 14;
then y in C /\ (south_halfline p) by A9, XBOOLE_0:def 4;
then A18: y `2 in proj2 .: (C /\ (south_halfline p)) by A16, FUNCT_2:43;
C /\ (south_halfline p) is Bounded by A11, TOPREAL6:98;
then proj2 .: (C /\ (south_halfline p)) is bounded by JCT_MISC:23;
then proj2 .: (C /\ (south_halfline p)) is bounded_above by XXREAL_2:def 11;
then y `2 <= (South-Bound (p,C)) `2 by A4, A18, SEQ_4:def 4;
then y `2 = (South-Bound (p,C)) `2 by A14, XXREAL_0:1;
hence y = South-Bound (p,C) by A5, A8, TOPREAL3:11; :: thesis: verum

end;

hence x in {(North-Bound (p,C)),(South-Bound (p,C))} by TARSKI:def 2; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( 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))} ; :: thesis: x in (LSeg ((North-Bound (p,C)),(South-Bound (p,C)))) /\ C
then A19: ( 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:69;
hence x in (LSeg ((North-Bound (p,C)),(South-Bound (p,C)))) /\ C by A19, A2, XBOOLE_0:def 4; :: thesis: verum