let A be non empty Subset of GRZ-formula-set; :: thesis: for R being GRZ-rule
for t being GRZ-formula holds
( A,R |- t iff ex S being GRZ-formula-finset st
( t in S & S is A,R -correct ) )
let R be GRZ-rule; :: thesis: for t being GRZ-formula holds
( A,R |- t iff ex S being GRZ-formula-finset st
( t in S & S is A,R -correct ) )
let t be GRZ-formula; :: thesis: ( A,R |- t iff ex S being GRZ-formula-finset st
( t in S & S is A,R -correct ) )
thus ( A,R |- t implies ex S being GRZ-formula-finset st
( t in S & S is A,R -correct ) ) :: thesis: ( ex S being GRZ-formula-finset st
( t in S & S is A,R -correct ) implies A,R |- t )

proof

assume A,R |- t ; :: thesis: ex S being GRZ-formula-finset st
( t in S & S is A,R -correct )
then consider P being GRZ-formula-sequence such that
A1: t in rng P and
A2: P is A,R -correct ;
take S = rng P; :: thesis: ( t in S & S is A,R -correct )
thus ( t in S & S is A,R -correct ) by A1, A2; :: thesis: verum

end;

given S being GRZ-formula-finset such that A10: t in S and
A11: S is A,R -correct ; :: thesis: A,R |- t
consider P being GRZ-formula-sequence such that
A12: S = rng P and
A13: P is A,R -correct by A11;
thus A,R |- t by A10, A12, A13; :: thesis: verum