let A be non empty Subset of GRZ-formula-set; :: thesis: 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; :: thesis: ( 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 ) ; :: thesis: 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
proof
let a be object ; :: thesis: ( a in {t,(t '=' u)} implies a in GRZ-formula-set )
assume a in {t,(t '=' u)} ; :: thesis: a in GRZ-formula-set
then ( a = t or a = t '=' u ) by TARSKI:def 2;
hence a in GRZ-formula-set ; :: thesis: verum
end;
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; :: thesis: verum