:: deftheorem defines .allWalks() GLIB_001:def 33 :
for G being _Graph holds G .allWalks() = { W where W is Walk of G : verum } ;