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

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