let A be non empty Subset of GRZ-formula-set; :: thesis: for R being GRZ-rule
for a being Element of A holds <*a*> is A,R -correct
let R be GRZ-rule; :: thesis: for a being Element of A holds <*a*> is A,R -correct
let a be Element of A; :: thesis: <*a*> is A,R -correct
set P = <*a*>;
let k be Element of NAT ; :: according to GRZLOG_1:def 30 :: thesis: ( k in dom <*a*> implies <*a*>,k is_a_correct_step_wrt A,R )
assume k in dom <*a*> ; :: thesis: <*a*>,k is_a_correct_step_wrt A,R
then <*a*> . k in rng <*a*> by FUNCT_1:3;
then <*a*> . k in {a} by FINSEQ_1:38;
then <*a*> . k = a by TARSKI:def 1;
hence <*a*>,k is_a_correct_step_wrt A,R ; :: thesis: verum