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

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