z9 <> z by DIFF;
hence z9 -term is z -omitting by ThC1; :: thesis: verum