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