theorem Th40: :: GRZLOG_1:9

for A being non empty Subset of GRZ-formula-set
for R being GRZ-rule
for a being Element of A holds <*a*> is A,R -correct