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)} )
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)}
set L = LSeg (North-Bound p,C),(South-Bound p,C);

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

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)} )
assume A2: 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) ;
A3: (South-Bound p,C) `1 = p `1 by EUCLID:56;
A4: (North-Bound p,C) `1 = p `1 by EUCLID:56;
A5: (South-Bound p,C) `2 = sup (proj2 .: (C /\ (south_halfline p))) by EUCLID:56;
A6: (North-Bound p,C) `2 = inf (proj2 .: (C /\ (north_halfline p))) by EUCLID:56;
A7: LSeg (North-Bound p,C),(South-Bound p,C) is vertical by Th26;
A8: South-Bound p,C in LSeg (North-Bound p,C),(South-Bound p,C) by RLTOPSP1:69;
A9: x in C by A2, XBOOLE_0:def 4;
A10: x in LSeg (North-Bound p,C),(South-Bound p,C) by A2, XBOOLE_0:def 4;
then A11: y `1 = p `1 by A3, A7, A8, SPPOL_1:def 3;

now

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

now

assume y `2 > p `2 ; :: thesis: contradiction
then y in north_halfline p by A11, 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 A18, FUNCT_2:43;
hence contradiction by A6, A14, A17, SEQ_4:def 5; :: thesis: verum

end;

then y in south_halfline p by A11, TOPREAL1:def 14;
then y in C /\ (south_halfline p) by A9, XBOOLE_0:def 4;
then y `2 in proj2 .: (C /\ (south_halfline p)) by A18, FUNCT_2:43;
then y `2 <= (South-Bound p,C) `2 by A5, A16, SEQ_4:def 4;
then y `2 = (South-Bound p,C) `2 by A13, XXREAL_0:1;
hence y = South-Bound p,C by A3, A11, 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;
A20: ( North-Bound p,C in C & South-Bound p,C in C ) by A1, Th22;
x in LSeg (North-Bound p,C),(South-Bound p,C) by A19, RLTOPSP1:69;
hence x in (LSeg (North-Bound p,C),(South-Bound p,C)) /\ C by A19, A20, XBOOLE_0:def 4; :: thesis: verum