:: deftheorem Def1 defines Chain MSSCYC_1:def 1 :
for G being Graph
for b₂ being set holds
( b₂ is Chain of G iff ( b₂ is FinSequence of the carrier' of G & ex p being FinSequence of the carrier of G st p is_vertex_seq_of b₂ ) );