:: deftheorem defines .allTrails() GLIB_001:def 34 :
for G being _Graph holds G .allTrails() = { W where W is Trail of G : verum } ;