let A be non empty Subset of GRZ-formula-set; for t, u being GRZ-formula st A, GRZ-rules |- t & A, GRZ-rules |- t '=' u holds
A, GRZ-rules |- u
let t, u be GRZ-formula; ( A, GRZ-rules |- t & A, GRZ-rules |- t '=' u implies A, GRZ-rules |- u )
assume A1:
( A, GRZ-rules |- t & A, GRZ-rules |- t '=' u )
; A, GRZ-rules |- u
set S = {t,(t '=' u)};
for a being object st a in {t,(t '=' u)} holds
a in GRZ-formula-set
then
{t,(t '=' u)} c= GRZ-formula-set
;
then reconsider S = {t,(t '=' u)} as GRZ-formula-finset ;
A3:
A, GRZ-rules |- S
by A1, TARSKI:def 2;
[S,u] in GRZ-MP
;
then
[S,u] in GRZ-rules
by Def35;
hence
A, GRZ-rules |- u
by A3, Th48; verum