len (vertex-seq oc) = (len oc) + 1 by Th9;
hence not vertex-seq oc is empty ; :: thesis: verum