:: deftheorem defines .allForests() GLENUM00:def 9 :
for G being _Graph holds G .allForests() = { H where H is Element of [#] (G .allSG()) : H is acyclic } ;