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