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 V5() )
thus ( G .walkOf the Vertex of G is closed & G .walkOf the Vertex of G is directed & G .walkOf the Vertex of G is V5() ) by Lm4; :: thesis: verum