reconsider H = G as Subgraph of G by GLIB_000:40;
take H ; :: thesis: not H is acyclic
thus not H is acyclic ; :: thesis: verum