let G1, G2 be _Graph; :: thesis: for F being non empty one-to-one PGraphMapping of G1,G2

for W1 being b_{1} -defined Walk of G1 holds

( ( W1 is V5() implies F .: W1 is V5() ) & ( F .: W1 is V5() implies W1 is V5() ) & ( W1 is closed implies F .: W1 is closed ) & ( F .: W1 is closed implies W1 is closed ) & ( W1 is Trail-like implies F .: W1 is Trail-like ) & ( F .: W1 is Trail-like implies W1 is Trail-like ) & ( W1 is Path-like implies F .: W1 is Path-like ) & ( F .: W1 is Path-like implies W1 is Path-like ) & ( W1 is Circuit-like implies F .: W1 is Circuit-like ) & ( F .: W1 is Circuit-like implies W1 is Circuit-like ) & ( W1 is Cycle-like implies F .: W1 is Cycle-like ) & ( F .: W1 is Cycle-like implies W1 is Cycle-like ) )

let F be non empty one-to-one PGraphMapping of G1,G2; :: thesis: for W1 being F -defined Walk of G1 holds

( ( W1 is V5() implies F .: W1 is V5() ) & ( F .: W1 is V5() implies W1 is V5() ) & ( W1 is closed implies F .: W1 is closed ) & ( F .: W1 is closed implies W1 is closed ) & ( W1 is Trail-like implies F .: W1 is Trail-like ) & ( F .: W1 is Trail-like implies W1 is Trail-like ) & ( W1 is Path-like implies F .: W1 is Path-like ) & ( F .: W1 is Path-like implies W1 is Path-like ) & ( W1 is Circuit-like implies F .: W1 is Circuit-like ) & ( F .: W1 is Circuit-like implies W1 is Circuit-like ) & ( W1 is Cycle-like implies F .: W1 is Cycle-like ) & ( F .: W1 is Cycle-like implies W1 is Cycle-like ) )

let W1 be F -defined Walk of G1; :: thesis: ( ( W1 is V5() implies F .: W1 is V5() ) & ( F .: W1 is V5() implies W1 is V5() ) & ( W1 is closed implies F .: W1 is closed ) & ( F .: W1 is closed implies W1 is closed ) & ( W1 is Trail-like implies F .: W1 is Trail-like ) & ( F .: W1 is Trail-like implies W1 is Trail-like ) & ( W1 is Path-like implies F .: W1 is Path-like ) & ( F .: W1 is Path-like implies W1 is Path-like ) & ( W1 is Circuit-like implies F .: W1 is Circuit-like ) & ( F .: W1 is Circuit-like implies W1 is Circuit-like ) & ( W1 is Cycle-like implies F .: W1 is Cycle-like ) & ( F .: W1 is Cycle-like implies W1 is Cycle-like ) )

W1 = F " (F .: W1) by Th123;

hence A1: ( ( W1 is V5() implies F .: W1 is V5() ) & ( F .: W1 is V5() implies W1 is V5() ) & ( W1 is closed implies F .: W1 is closed ) & ( F .: W1 is closed implies W1 is closed ) & ( W1 is Trail-like implies F .: W1 is Trail-like ) & ( F .: W1 is Trail-like implies W1 is Trail-like ) & ( W1 is Path-like implies F .: W1 is Path-like ) & ( F .: W1 is Path-like implies W1 is Path-like ) ) by Th137; :: thesis: ( ( W1 is Circuit-like implies F .: W1 is Circuit-like ) & ( F .: W1 is Circuit-like implies W1 is Circuit-like ) & ( W1 is Cycle-like implies F .: W1 is Cycle-like ) & ( F .: W1 is Cycle-like implies W1 is Cycle-like ) )

thus ( W1 is Circuit-like iff F .: W1 is Circuit-like ) by A1; :: thesis: ( W1 is Cycle-like iff F .: W1 is Cycle-like )

thus ( W1 is Cycle-like iff F .: W1 is Cycle-like ) by A1; :: thesis: verum

for W1 being b

( ( W1 is V5() implies F .: W1 is V5() ) & ( F .: W1 is V5() implies W1 is V5() ) & ( W1 is closed implies F .: W1 is closed ) & ( F .: W1 is closed implies W1 is closed ) & ( W1 is Trail-like implies F .: W1 is Trail-like ) & ( F .: W1 is Trail-like implies W1 is Trail-like ) & ( W1 is Path-like implies F .: W1 is Path-like ) & ( F .: W1 is Path-like implies W1 is Path-like ) & ( W1 is Circuit-like implies F .: W1 is Circuit-like ) & ( F .: W1 is Circuit-like implies W1 is Circuit-like ) & ( W1 is Cycle-like implies F .: W1 is Cycle-like ) & ( F .: W1 is Cycle-like implies W1 is Cycle-like ) )

let F be non empty one-to-one PGraphMapping of G1,G2; :: thesis: for W1 being F -defined Walk of G1 holds

( ( W1 is V5() implies F .: W1 is V5() ) & ( F .: W1 is V5() implies W1 is V5() ) & ( W1 is closed implies F .: W1 is closed ) & ( F .: W1 is closed implies W1 is closed ) & ( W1 is Trail-like implies F .: W1 is Trail-like ) & ( F .: W1 is Trail-like implies W1 is Trail-like ) & ( W1 is Path-like implies F .: W1 is Path-like ) & ( F .: W1 is Path-like implies W1 is Path-like ) & ( W1 is Circuit-like implies F .: W1 is Circuit-like ) & ( F .: W1 is Circuit-like implies W1 is Circuit-like ) & ( W1 is Cycle-like implies F .: W1 is Cycle-like ) & ( F .: W1 is Cycle-like implies W1 is Cycle-like ) )

let W1 be F -defined Walk of G1; :: thesis: ( ( W1 is V5() implies F .: W1 is V5() ) & ( F .: W1 is V5() implies W1 is V5() ) & ( W1 is closed implies F .: W1 is closed ) & ( F .: W1 is closed implies W1 is closed ) & ( W1 is Trail-like implies F .: W1 is Trail-like ) & ( F .: W1 is Trail-like implies W1 is Trail-like ) & ( W1 is Path-like implies F .: W1 is Path-like ) & ( F .: W1 is Path-like implies W1 is Path-like ) & ( W1 is Circuit-like implies F .: W1 is Circuit-like ) & ( F .: W1 is Circuit-like implies W1 is Circuit-like ) & ( W1 is Cycle-like implies F .: W1 is Cycle-like ) & ( F .: W1 is Cycle-like implies W1 is Cycle-like ) )

W1 = F " (F .: W1) by Th123;

hence A1: ( ( W1 is V5() implies F .: W1 is V5() ) & ( F .: W1 is V5() implies W1 is V5() ) & ( W1 is closed implies F .: W1 is closed ) & ( F .: W1 is closed implies W1 is closed ) & ( W1 is Trail-like implies F .: W1 is Trail-like ) & ( F .: W1 is Trail-like implies W1 is Trail-like ) & ( W1 is Path-like implies F .: W1 is Path-like ) & ( F .: W1 is Path-like implies W1 is Path-like ) ) by Th137; :: thesis: ( ( W1 is Circuit-like implies F .: W1 is Circuit-like ) & ( F .: W1 is Circuit-like implies W1 is Circuit-like ) & ( W1 is Cycle-like implies F .: W1 is Cycle-like ) & ( F .: W1 is Cycle-like implies W1 is Cycle-like ) )

thus ( W1 is Circuit-like iff F .: W1 is Circuit-like ) by A1; :: thesis: ( W1 is Cycle-like iff F .: W1 is Cycle-like )

thus ( W1 is Cycle-like iff F .: W1 is Cycle-like ) by A1; :: thesis: verum