set v = the Element of rng (F _V);

reconsider v = the Element of rng (F _V) as Vertex of G2 ;

set W2 = G2 .walkOf v;

take G2 .walkOf v ; :: thesis: ( G2 .walkOf v is F -valued & G2 .walkOf v is V5() )

(G2 .walkOf v) .vertices() = {v} by GLIB_001:90;

hence (G2 .walkOf v) .vertices() c= rng (F _V) by ZFMISC_1:31; :: according to GLIB_010:def 36 :: thesis: ( (G2 .walkOf v) .edges() c= rng (F _E) & G2 .walkOf v is V5() )

thus (G2 .walkOf v) .edges() c= rng (F _E) by XBOOLE_1:2; :: thesis: G2 .walkOf v is V5()

thus G2 .walkOf v is V5() ; :: thesis: verum

reconsider v = the Element of rng (F _V) as Vertex of G2 ;

set W2 = G2 .walkOf v;

take G2 .walkOf v ; :: thesis: ( G2 .walkOf v is F -valued & G2 .walkOf v is V5() )

(G2 .walkOf v) .vertices() = {v} by GLIB_001:90;

hence (G2 .walkOf v) .vertices() c= rng (F _V) by ZFMISC_1:31; :: according to GLIB_010:def 36 :: thesis: ( (G2 .walkOf v) .edges() c= rng (F _E) & G2 .walkOf v is V5() )

thus (G2 .walkOf v) .edges() c= rng (F _E) by XBOOLE_1:2; :: thesis: G2 .walkOf v is V5()

thus G2 .walkOf v is V5() ; :: thesis: verum