theorem :: GRZLOG_1:4

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