:: deftheorem defines .allDWalks() GLIB_001:def 36 :
for G being _Graph holds G .allDWalks() = { W where W is DWalk of G : verum } ;