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;

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

(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

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

end;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) )

hence
x in {(North-Bound (p,C)),(South-Bound (p,C))}
by TARSKI:def 2; :: thesis: verum
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;

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

then
y in south_halfline p
by A8, TOPREAL1:def 12;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 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

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

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