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 )
assume A1: A is_a_component_of GX ; :: thesis: A is closed
A2: A c= Cl A by PRE_TOPC:48;
A is connected by A1, Def5;
then Cl A is connected by Th20;
then A = Cl A by A1, A2, Def5;
hence A is closed by PRE_TOPC:52; :: thesis: verum