set W = GRZ-formula-set ;
set U = [:(bool GRZ-formula-set),GRZ-formula-set:];
defpred S₁[ object ] means ( $1 in GRZ-MP or $1 in GRZ-ConjIntro or $1 in GRZ-ConjElimL or $1 in GRZ-ConjElimR );
consider X being set such that
A1: for a being object holds
( a in X iff ( a in [:(bool GRZ-formula-set),GRZ-formula-set:] & S₁[a] ) ) from XBOOLE_0:sch 1();
X c= [:(bool GRZ-formula-set),GRZ-formula-set:] by A1;
then reconsider X = X as GRZ-rule ;
take X ; :: thesis: for a being object holds
( a in X iff ( a in GRZ-MP or a in GRZ-ConjIntro or a in GRZ-ConjElimL or a in GRZ-ConjElimR ) )
thus for a being object holds
( a in X iff ( a in GRZ-MP or a in GRZ-ConjIntro or a in GRZ-ConjElimL or a in GRZ-ConjElimR ) ) by A1; :: thesis: verum