let G1, G2 be _Graph; :: thesis: for F being non empty one-to-one PGraphMapping of G1,G2
for H2 being acyclic Subgraph of rng F
for H1 being inducedSubgraph of G1,(F _V) " (the_Vertices_of H2),(F _E) " (the_Edges_of H2) holds H1 is acyclic
let F be non empty one-to-one PGraphMapping of G1,G2; :: thesis: for H2 being acyclic Subgraph of rng F
for H1 being inducedSubgraph of G1,(F _V) " (the_Vertices_of H2),(F _E) " (the_Edges_of H2) holds H1 is acyclic
let H2 be acyclic Subgraph of rng F; :: thesis: for H1 being inducedSubgraph of G1,(F _V) " (the_Vertices_of H2),(F _E) " (the_Edges_of H2) holds H1 is acyclic
let H1 be inducedSubgraph of G1,(F _V) " (the_Vertices_of H2),(F _E) " (the_Edges_of H2); :: thesis: H1 is acyclic
assume not H1 is acyclic ; :: thesis: contradiction
then consider W1 being Walk of H1 such that
A1: W1 is Cycle-like by GLIB_002:def 2;
reconsider W = W1 as F -defined Walk of G1 by Th106;
W is Cycle-like by A1, GLIB_006:24;
then A2: F .: W is Cycle-like by GLIB_010:138;
reconsider W2 = F .: W as Walk of H2 by Th107;
W2 is Cycle-like by A2, GLIB_006:24;
hence contradiction by GLIB_002:def 2; :: thesis: verum