:: deftheorem defines .allComponents() GLENUM00:def 15 :
for G being _Graph holds G .allComponents() = { H where H is Element of [#] (G .allSG()) : H is Component-like } ;