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 Th17;

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:52;
A4: (South-Bound (p,C)) `2 = upper_bound (proj2 .: (C /\ (south_halfline p))) by EUCLID:52;
let x be object ; :: 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:52;
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 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 :: thesis: ( 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) ; :: thesis: 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;

now :: thesis: not y `2 > p `2

assume y `2 > p `2 ; :: thesis: contradiction
then y in north_halfline p by A8, TOPREAL1:def 10;
then y in C /\ (north_halfline p) by A9, XBOOLE_0:def 4;
then y `2 in proj2 .: (C /\ (north_halfline p)) by A15, FUNCT_2:35;
hence contradiction by A3, A16, A11, SEQ_4:def 2; :: thesis: verum

end;

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; :: thesis: verum

end;

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

end;

let x be object ; :: 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 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; :: thesis: verum