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