defpred S₁[ object ] means ( $1 in GRZ-MP or $1 in GRZ-ConjIntro or $1 in GRZ-ConjElimL or $1 in GRZ-ConjElimR );
let X1, X2 be GRZ-rule; :: thesis: ( ( for a being object holds
( a in X1 iff ( a in GRZ-MP or a in GRZ-ConjIntro or a in GRZ-ConjElimL or a in GRZ-ConjElimR ) ) ) & ( for a being object holds
( a in X2 iff ( a in GRZ-MP or a in GRZ-ConjIntro or a in GRZ-ConjElimL or a in GRZ-ConjElimR ) ) ) implies X1 = X2 )
assume that
A1: for a being object holds
( a in X1 iff S₁[a] ) and
A2: for a being object holds
( a in X2 iff S₁[a] ) ; :: thesis: X1 = X2
thus X1 = X2 from XBOOLE_0:sch 2(A1, A2); :: thesis: verum