defpred S₁[ object ] means ex t, u, v being GRZ-formula st
( $1 = (t '=' u) => ((t '&' v) '=' (u '&' v)) or $1 = (t '=' u) => ((t 'or' v) '=' (u 'or' v)) or $1 = (t '=' u) => ((t '=' v) '=' (u '=' v)) );
let X1, X2 be non empty Subset of GRZ-formula-set; :: thesis: ( ( for a being object holds
( a in X1 iff ex t, u, v being GRZ-formula st
( a = (t '=' u) => ((t '&' v) '=' (u '&' v)) or a = (t '=' u) => ((t 'or' v) '=' (u 'or' v)) or a = (t '=' u) => ((t '=' v) '=' (u '=' v)) ) ) ) & ( for a being object holds
( a in X2 iff ex t, u, v being GRZ-formula st
( a = (t '=' u) => ((t '&' v) '=' (u '&' v)) or a = (t '=' u) => ((t 'or' v) '=' (u 'or' v)) or a = (t '=' u) => ((t '=' v) '=' (u '=' v)) ) ) ) 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