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 Th18, SUBSET_1:10;
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 Th90;
hence contradiction by A1, A5, A4, RLTOPSP1:42, XBOOLE_1:73; :: thesis: verum

end;

WH c= C ` by A2, SUBSET_1:23;
hence WH c= UBD C by A3, Th108, GOBOARD9:4; :: thesis: verum