for t being GRZ-formula holds
( t is atomic iff t in VAR ) by Th5;