given a being object such that A1: a in VAR and
A2: a in GRZ-ops ; :: thesis: contradiction
reconsider p = a as Element of GRZ-symbols by A1, XBOOLE_0:def 3;
p . 1 = 0 by A1, Lm1;
hence contradiction by A2, Lm2; :: thesis: verum