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