let G2 be Supergraph of G; :: thesis: not G2 is acyclic
A1: G is Subgraph of G2 by Th61;
assume G2 is acyclic ; :: thesis: contradiction
hence contradiction by A1; :: thesis: verum