A1: <*0,n*> in Polish-atoms (GRZ-symbols,GRZ-arity) by Th5;
Polish-atoms (GRZ-symbols,GRZ-arity) c= Polish-expression-set (GRZ-symbols,GRZ-arity) by POLNOT_1:36;
hence <*0,n*> is GRZ-formula by A1, POLNOT_1:def 25; :: thesis: verum