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

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

hence
G1 is acyclic
by GLIB_002:def 2; :: thesis: verum
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;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