union { B where B is Subset of (TOP-REAL n) : B is_outside_component_of A } c= the carrier of (TOP-REAL n)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in union { B where B is Subset of (TOP-REAL n) : B is_outside_component_of A } or x in the carrier of (TOP-REAL n) )
assume x in union { B where B is Subset of (TOP-REAL n) : B is_outside_component_of A } ; :: thesis: x in the carrier of (TOP-REAL n)
then consider y being set such that
A1: ( x in y & y in { B where B is Subset of (TOP-REAL n) : B is_outside_component_of A } ) by TARSKI:def 4;
consider B being Subset of (TOP-REAL n) such that
A2: ( y = B & B is_outside_component_of A ) by A1;
thus x in the carrier of (TOP-REAL n) by A1, A2; :: thesis: verum

end;

hence union { B where B is Subset of (TOP-REAL n) : B is_outside_component_of A } is Subset of (TOP-REAL n) ; :: thesis: verum