let G1, G2 be _Graph; :: thesis: for F being PGraphMapping of G1,G2 st F is strong_SG-embedding & G2 is acyclic holds
G1 is acyclic
let F be PGraphMapping of G1,G2; :: thesis: ( F is strong_SG-embedding & G2 is acyclic implies G1 is acyclic )
assume A1: F is strong_SG-embedding ; :: thesis: ( not G2 is acyclic or G1 is acyclic )
then reconsider F = F as non empty one-to-one PGraphMapping of G1,G2 ;
assume A2: G2 is acyclic ; :: thesis: G1 is acyclic
for W1 being Walk of G1 holds not W1 is Cycle-like
proof
given W1 being Walk of G1 such that A3: W1 is Cycle-like ; :: thesis: contradiction
reconsider W1 = W1 as F -defined Walk of G1 by A1, Th121;
F .: W1 is Cycle-like by A3, Th138;
hence contradiction by A2, GLIB_002:def 2; :: thesis: verum
end;
hence G1 is acyclic by GLIB_002:def 2; :: thesis: verum