consider y being Element of Z . s such that
A1: y <> z by SUBSET_1:50;
take y -term ; :: thesis: y -term is z -omitting
thus y -term is z -omitting by A1, ThC1; :: thesis: verum