let n be Nat; :: thesis: for A being Subset of (TOP-REAL n) holds (BDD A) \/ (UBD A) = A `
let A be Subset of (TOP-REAL n); :: thesis: (BDD A) \/ (UBD A) = A `
A1: A ` c= (BDD A) \/ (UBD A)

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in A ` or z in (BDD A) \/ (UBD A) )
assume A2: z in A ` ; :: thesis: z in (BDD A) \/ (UBD A)
then reconsider p = z as Element of A ` ;
reconsider B = A ` as non empty Subset of (TOP-REAL n) by A2;
reconsider q = p as Point of ((TOP-REAL n) | (A `)) by PRE_TOPC:8;
Component_of q is Subset of ([#] ((TOP-REAL n) | (A `))) ;
then Component_of q is Subset of (A `) by PRE_TOPC:def 5;
then reconsider G = Component_of q as Subset of (TOP-REAL n) by XBOOLE_1:1;
A3: not (TOP-REAL n) | B is empty ;
then A4: q in G by CONNSP_1:38;
Component_of q is a_component by A3, CONNSP_1:40;
then A5: G is_a_component_of A ` by CONNSP_1:def 6;

per cases ( G is bounded or not G is bounded ) ;

suppose G is bounded ; :: thesis: z in (BDD A) \/ (UBD A)

then G is_inside_component_of A by A5;
then G c= BDD A by Th13;
hence z in (BDD A) \/ (UBD A) by A4, XBOOLE_0:def 3; :: thesis: verum

end;

suppose not G is bounded ; :: thesis: z in (BDD A) \/ (UBD A)

then G is_outside_component_of A by A5;
then G c= UBD A by Th14;
hence z in (BDD A) \/ (UBD A) by A4, XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

( BDD A c= A ` & UBD A c= A ` ) by Th16, Th17;
then (BDD A) \/ (UBD A) c= A ` by XBOOLE_1:8;
hence (BDD A) \/ (UBD A) = A ` by A1; :: thesis: verum