set X = GRZ-formula-set ;
set Y = [:(bool GRZ-formula-set),GRZ-formula-set:];
set Z = { [{t,u},(t '&' u)] where t, u is GRZ-formula : verum } ;
{ [{t,u},(t '&' u)] where t, u is GRZ-formula : verum } c= [:(bool GRZ-formula-set),GRZ-formula-set:]

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { [{t,u},(t '&' u)] where t, u is GRZ-formula : verum } or a in [:(bool GRZ-formula-set),GRZ-formula-set:] )
assume a in { [{t,u},(t '&' 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,u},(t '&' u)] ;
set w = {t,u};
( t in GRZ-formula-set & u in GRZ-formula-set ) ;
then {t,u} c= GRZ-formula-set by TARSKI:def 2;
then {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;

hence { [{t,u},(t '&' u)] where t, u is GRZ-formula : verum } is GRZ-rule ; :: thesis: verum