let S be Graph-membered set ; :: thesis: ( S is Cycle-like implies S is connected )
assume A1: S is Cycle-like ; :: thesis: S is connected

now :: thesis: for G being _Graph st G in S holds
G is connected

let G be _Graph; :: thesis: ( G in S implies G is connected )
assume G in S ; :: thesis: G is connected
then G is Cycle-like by A1;
hence G is connected ; :: thesis: verum

end;

hence S is connected by GLIB_014:def 9; :: thesis: verum