let GX be TopSpace; :: thesis: for A being Subset of GX st A is_a_component_of GX holds
A is closed
let A be Subset of GX; :: thesis: ( A is_a_component_of GX implies A is closed )
A1: A c= Cl A by PRE_TOPC:48;
assume A2: A is_a_component_of GX ; :: thesis: A is closed
then A is connected by Def5;
then Cl A is connected by Th20;
then A = Cl A by A2, A1, Def5;
hence A is closed by PRE_TOPC:52; :: thesis: verum