:: deftheorem defines .allPaths() GLIB_001:def 35 :
for G being _Graph holds G .allPaths() = { W where W is Path of G : verum } ;