let C1 be Cycle-like _Graph; :: thesis: for C2 being non acyclic Subgraph of C1 holds C1 == C2
let C2 be non acyclic Subgraph of C1; :: thesis: C1 == C2
consider W2 being Walk of C2 such that
A1: W2 is Cycle-like by GLIB_002:def 2;
reconsider W1 = W2 as Walk of C1 by GLIB_001:167;
W1 is Cycle-like by A1, GLIB_006:24;
then ( W1 .vertices() = the_Vertices_of C1 & W1 .edges() = the_Edges_of C1 ) by Th39;
then ( W2 .vertices() = the_Vertices_of C1 & W2 .edges() = the_Edges_of C1 ) by GLIB_001:98, GLIB_001:110;
then A2: ( the_Vertices_of C1 c= the_Vertices_of C2 & the_Edges_of C1 c= the_Edges_of C2 ) ;
C1 is Subgraph of C1 by GLIB_000:40;
then C1 is Subgraph of C2 by A2, GLIB_000:44;
hence C1 == C2 by GLIB_000:87; :: thesis: verum