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 trivial )
(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 trivial )
thus (G2 .walkOf v) .edges() c= rng (F _E) by XBOOLE_1:2; :: thesis: G2 .walkOf v is trivial
thus G2 .walkOf v is trivial ; :: thesis: verum