for G being Graph holds
( G is connected iff for v1, v2 being Vertex of G st v1 <> v2 holds
ex c being Chain of G ex vs being FinSequence of the carrier of G st
( not c is empty & vs is_vertex_seq_of c & vs . 1 = v1 & vs . (len vs) = v2 ) )