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