set X = GRZ-formula-set ;
set Y = [:(bool GRZ-formula-set),GRZ-formula-set:];
set Z = { [{t,(t '=' u)},u] where t, u is GRZ-formula : verum } ;
for a being object st a in { [{t,(t '=' u)},u] where t, u is GRZ-formula : verum } holds
a in [:(bool GRZ-formula-set),GRZ-formula-set:]

proof

let a be object ; :: thesis: ( a in { [{t,(t '=' u)},u] where t, u is GRZ-formula : verum } implies a in [:(bool GRZ-formula-set),GRZ-formula-set:] )
assume a in { [{t,(t '=' u)},u] where t, u is GRZ-formula : verum } ; :: thesis: a in [:(bool GRZ-formula-set),GRZ-formula-set:]
then consider t, u being GRZ-formula such that
A2: a = [{t,(t '=' u)},u] ;
set w = {t,(t '=' u)};
( t in GRZ-formula-set & t '=' u in GRZ-formula-set ) ;
then {t,(t '=' u)} c= GRZ-formula-set by TARSKI:def 2;
then {t,(t '=' u)} in bool GRZ-formula-set by ZFMISC_1:def 1;
hence a in [:(bool GRZ-formula-set),GRZ-formula-set:] by A2, ZFMISC_1:def 2; :: thesis: verum

end;

then { [{t,(t '=' u)},u] where t, u is GRZ-formula : verum } c= [:(bool GRZ-formula-set),GRZ-formula-set:] ;
hence { [{t,(t '=' u)},u] where t, u is GRZ-formula : verum } is GRZ-rule ; :: thesis: verum