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 ;
( 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 }
;
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;
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
; verum