let W be Walk of G; :: thesis: W is V5()
W .edges() = {} ;
hence W is V5() by GLIB_001:136; :: thesis: verum