let C be compact Subset of (TOP-REAL 2); :: thesis: for WH being connected Subset of (TOP-REAL 2) st not WH is Bounded & WH misses C holds
WH c= UBD C
let WH be connected Subset of (TOP-REAL 2); :: thesis: ( not WH is Bounded & WH misses C implies WH c= UBD C )
assume that
A1: not WH is Bounded and
A2: WH misses C ; :: thesis: WH c= UBD C
A3: WH meets UBD C

proof

( (BDD C) \/ (UBD C) = C ` & [#] the carrier of (TOP-REAL 2) = C \/ (C ` ) ) by Th31, SUBSET_1:25;
then A4: WH c= (UBD C) \/ (BDD C) by A2, XBOOLE_1:73;
assume A5: WH misses UBD C ; :: thesis: contradiction
BDD C is Bounded by Th114;
hence contradiction by A1, A5, A4, Th16, XBOOLE_1:73; :: thesis: verum

end;

WH c= C ` by A2, SUBSET_1:43;
hence WH c= UBD C by A3, Th132, GOBOARD9:6; :: thesis: verum