set X = GRZ-formula-set ;
set Y = [:(bool GRZ-formula-set),GRZ-formula-set:];
set Z = { [{(t '&' u)},u] where t, u is GRZ-formula : verum } ;
{ [{(t '&' u)},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)},u] where t, u is GRZ-formula : verum } or a in [:(bool GRZ-formula-set),GRZ-formula-set:] )
assume a in { [{(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 '&' u)},u] ;
set w = {(t '&' u)};
t '&' u in GRZ-formula-set ;
then {(t '&' u)} c= GRZ-formula-set by TARSKI:def 1;
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)},u] where t, u is GRZ-formula : verum } is GRZ-rule ; :: thesis: verum