let S be non empty non void identifying_close_blocks TopStruct ; :: thesis: ( S is strongly_connected implies S is connected )
assume A1: S is strongly_connected ; :: thesis: S is connected
then S is without_isolated_points by Th3;
hence S is connected by A1, PENCIL_1:28; :: thesis: verum