let G1, G2 be _Graph; :: thesis: ( G1 == G2 & G1 is acyclic implies G2 is acyclic )
assume that
A1: G1 == G2 and
A2: G1 is acyclic ; :: thesis: G2 is acyclic
reconsider G19 = G1 as acyclic _Graph by A2;
G2 is Subgraph of G19 by A1, GLIB_000:87;
hence G2 is acyclic ; :: thesis: verum