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

now :: thesis: for G being _Graph st G in S holds
G is Tree-like

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

end;

hence S is Tree-like by GLIB_014:def 10; :: thesis: verum