let G1, G2 be _Graph; :: thesis: for W1 being Walk of G1
for W2 being Walk of G2 st G1 == G2 & W1 = W2 holds
( ( W1 is closed implies W2 is closed ) & ( W2 is closed implies W1 is closed ) & ( W1 is directed implies W2 is directed ) & ( W2 is directed implies W1 is directed ) & ( W1 is trivial implies W2 is trivial ) & ( W2 is trivial implies W1 is trivial ) & ( W1 is Trail-like implies W2 is Trail-like ) & ( W2 is Trail-like implies W1 is Trail-like ) & ( W1 is Path-like implies W2 is Path-like ) & ( W2 is Path-like implies W1 is Path-like ) & ( W1 is vertex-distinct implies W2 is vertex-distinct ) & ( W2 is vertex-distinct implies W1 is vertex-distinct ) )
let W1 be Walk of G1; :: thesis: for W2 being Walk of G2 st G1 == G2 & W1 = W2 holds
( ( W1 is closed implies W2 is closed ) & ( W2 is closed implies W1 is closed ) & ( W1 is directed implies W2 is directed ) & ( W2 is directed implies W1 is directed ) & ( W1 is trivial implies W2 is trivial ) & ( W2 is trivial implies W1 is trivial ) & ( W1 is Trail-like implies W2 is Trail-like ) & ( W2 is Trail-like implies W1 is Trail-like ) & ( W1 is Path-like implies W2 is Path-like ) & ( W2 is Path-like implies W1 is Path-like ) & ( W1 is vertex-distinct implies W2 is vertex-distinct ) & ( W2 is vertex-distinct implies W1 is vertex-distinct ) )
let W2 be Walk of G2; :: thesis: ( G1 == G2 & W1 = W2 implies ( ( W1 is closed implies W2 is closed ) & ( W2 is closed implies W1 is closed ) & ( W1 is directed implies W2 is directed ) & ( W2 is directed implies W1 is directed ) & ( W1 is trivial implies W2 is trivial ) & ( W2 is trivial implies W1 is trivial ) & ( W1 is Trail-like implies W2 is Trail-like ) & ( W2 is Trail-like implies W1 is Trail-like ) & ( W1 is Path-like implies W2 is Path-like ) & ( W2 is Path-like implies W1 is Path-like ) & ( W1 is vertex-distinct implies W2 is vertex-distinct ) & ( W2 is vertex-distinct implies W1 is vertex-distinct ) ) )
assume A1: ( G1 == G2 & W1 = W2 ) ; :: thesis: ( ( W1 is closed implies W2 is closed ) & ( W2 is closed implies W1 is closed ) & ( W1 is directed implies W2 is directed ) & ( W2 is directed implies W1 is directed ) & ( W1 is trivial implies W2 is trivial ) & ( W2 is trivial implies W1 is trivial ) & ( W1 is Trail-like implies W2 is Trail-like ) & ( W2 is Trail-like implies W1 is Trail-like ) & ( W1 is Path-like implies W2 is Path-like ) & ( W2 is Path-like implies W1 is Path-like ) & ( W1 is vertex-distinct implies W2 is vertex-distinct ) & ( W2 is vertex-distinct implies W1 is vertex-distinct ) )
then G1 is Subgraph of G2 by GLIB_000:90;
hence ( ( W1 is closed implies W2 is closed ) & ( W2 is closed implies W1 is closed ) & ( W1 is directed implies W2 is directed ) & ( W2 is directed implies W1 is directed ) & ( W1 is trivial implies W2 is trivial ) & ( W2 is trivial implies W1 is trivial ) & ( W1 is Trail-like implies W2 is Trail-like ) & ( W2 is Trail-like implies W1 is Trail-like ) & ( W1 is Path-like implies W2 is Path-like ) & ( W2 is Path-like implies W1 is Path-like ) & ( W1 is vertex-distinct implies W2 is vertex-distinct ) & ( W2 is vertex-distinct implies W1 is vertex-distinct ) ) by A1, Th177; :: thesis: verum