let t be GRZ-formula; :: thesis: ( t is atomic implies not t is negative )
assume A1: t is atomic ; :: thesis: not t is negative
assume t is negative ; :: thesis: contradiction
then Polish-arity t = 1 by Th4, POLNOT_1:def 35;
hence contradiction by A1, POLNOT_1:84; :: thesis: verum