:: deftheorem Def8 defines -CycleSet GRAPH_3:def 8 :
for G being Graph
for b₂ being FinSequenceSet of the carrier' of G holds
( b₂ = G -CycleSet iff for x being set holds
( x in b₂ iff x is cyclic Path of G ) );