let n be Element of 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 A1: B is_outside_component_of A ; :: thesis: B c= UBD A
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in B or x in UBD A )
assume A2: x in B ; :: thesis: x in UBD A
B in { B2 where B2 is Subset of (TOP-REAL n) : B2 is_outside_component_of A } by A1;
hence x in UBD A by A2, TARSKI:def 4; :: thesis: verum