let p be Point of (); :: thesis: for C being compact Subset of () 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 (); :: 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 /\ ())) by EUCLID:52;
A4: (South-Bound (p,C)) `2 = upper_bound (proj2 .: (C /\ ())) 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 () ;
A7: x in LSeg ((North-Bound (p,C)),(South-Bound (p,C))) by ;
( 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 ;
then A8: y `1 = p `1 by ;
A9: x in C by ;
A10: (North-Bound (p,C)) `1 = p `1 by EUCLID:52;
now :: thesis: ( y <> North-Bound (p,C) implies y = South-Bound (p,C) )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 ; :: thesis: verum