let G1, G2 be _Graph; :: thesis: for F being non empty one-to-one PGraphMapping of G1,G2
for W1 being b₁ -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