let G be Graph; :: thesis: for c being Chain of G
for vs being FinSequence of the carrier of G st vs is_vertex_seq_of c holds
not vs is empty
let c be Chain of G; :: thesis: for vs being FinSequence of the carrier of G st vs is_vertex_seq_of c holds
not vs is empty
let vs be FinSequence of the carrier of G; :: thesis: ( vs is_vertex_seq_of c implies not vs is empty )
assume vs is_vertex_seq_of c ; :: thesis: not vs is empty
then len vs = (len c) + 1 by GRAPH_2:def 7;
hence not vs is empty ; :: thesis: verum