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

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in union { B where B is Subset of (TOP-REAL n) : B is_inside_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_inside_component_of A } ; :: thesis: x in the carrier of (TOP-REAL n)
then consider y being set such that
A1: x in y and
A2: y in { B where B is Subset of (TOP-REAL n) : B is_inside_component_of A } by TARSKI:def 4;
ex B being Subset of (TOP-REAL n) st
( y = B & B is_inside_component_of A ) by A2;
hence x in the carrier of (TOP-REAL n) by A1; :: thesis: verum

end;

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