let t be GRZ-formula; :: thesis: ( t is atomic or t is negative or t is conjunctive or t is being_equality )
set s = Polish-WFF-head t;
assume A1: ( not t is atomic & not t is negative & not t is conjunctive & not t is being_equality ) ; :: thesis: contradiction
then not Polish-WFF-head t in GRZ-ops by ENUMSET1:def 1;
then A2: Polish-WFF-head t in VAR by XBOOLE_0:def 3;
Polish-WFF-head t = GRZ-symbols -head t by POLNOT_1:def 33;
hence contradiction by A1, A2, Th5, POLNOT_1:69; :: thesis: verum