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