consider v being Vertex of G;
take G .walkOf v ; :: thesis: ( G .walkOf v is closed & G .walkOf v is directed & G .walkOf v is trivial )
thus ( G .walkOf v is closed & G .walkOf v is directed & G .walkOf v is trivial ) by Lm4; :: thesis: verum