:: deftheorem defines .allSpanningTrees() GLENUM00:def 14 :
for G being _Graph holds G .allSpanningTrees() = { H where H is Element of [#] (G .allSG()) : ( H is spanning & H is Tree-like ) } ;