let G be non void Graph; :: thesis: for oc being non empty directed Chain of G holds len (vertex-seq oc) = (len oc) + 1
let oc be non empty directed Chain of G; :: thesis: len (vertex-seq oc) = (len oc) + 1
vertex-seq oc is_vertex_seq_of oc by GRAPH_2:def 10;
hence len (vertex-seq oc) = (len oc) + 1 ; :: thesis: verum