take z1 -term ; :: thesis: ( z1 -term is z -omitting & z1 -term is z1 -context )
thus ( z1 -term is z -omitting & z1 -term is z1 -context ) ; :: thesis: verum