let A be Subset of GX; :: thesis: ( A is a_component implies A is closed )

A1: A c= Cl A by PRE_TOPC:18;

assume A2: A is a_component ; :: thesis: A is closed

then Cl A is connected by Th19;

then A = Cl A by A2, A1;

hence A is closed by PRE_TOPC:22; :: thesis: verum

A1: A c= Cl A by PRE_TOPC:18;

assume A2: A is a_component ; :: thesis: A is closed

then Cl A is connected by Th19;

then A = Cl A by A2, A1;

hence A is closed by PRE_TOPC:22; :: thesis: verum