let A be non empty Subset of GRZ-formula-set; :: thesis: for R being GRZ-rule
for t being GRZ-formula st t in A holds
A,R |- t
let R be GRZ-rule; :: thesis: for t being GRZ-formula st t in A holds
A,R |- t
let t be GRZ-formula; :: thesis: ( t in A implies A,R |- t )
assume t in A ; :: thesis: A,R |- t
then reconsider a = t as Element of A ;
set P = <*a*>;
take <*a*> ; :: according to GRZLOG_1:def 32 :: thesis: ( t in rng <*a*> & <*a*> is A,R -correct )
rng <*a*> = {a} by FINSEQ_1:38;
hence ( t in rng <*a*> & <*a*> is A,R -correct ) by TARSKI:def 1, Th40; :: thesis: verum