let n be Nat; :: thesis: for A, B being Subset of (TOP-REAL n) st B is_outside_component_of A holds
B c= UBD A
let A, B be Subset of (TOP-REAL n); :: thesis: ( B is_outside_component_of A implies B c= UBD A )
assume B is_outside_component_of A ; :: thesis: B c= UBD A
then A1: B in { B2 where B2 is Subset of (TOP-REAL n) : B2 is_outside_component_of A } ;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in B or x in UBD A )
assume x in B ; :: thesis: x in UBD A
hence x in UBD A by A1, TARSKI:def 4; :: thesis: verum