defpred S₁[ object ] means ex t, u, v being GRZ-formula st
( $1 = 'not' (t '&' ('not' t)) or $1 = ('not' ('not' t)) '=' t or $1 = t '=' (t '&' t) or $1 = (t '&' u) '=' (u '&' t) or $1 = (t '&' (u '&' v)) '=' ((t '&' u) '&' v) or $1 = (t '&' (u 'or' v)) '=' ((t '&' u) 'or' (t '&' v)) or $1 = ('not' (t '&' u)) '=' (('not' t) 'or' ('not' u)) or $1 = (t '=' u) '=' (u '=' t) or $1 = (t '=' u) '=' (('not' t) '=' ('not' u)) );
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 = 'not' (t '&' ('not' t)) or a = ('not' ('not' t)) '=' t or a = t '=' (t '&' t) or a = (t '&' u) '=' (u '&' t) or a = (t '&' (u '&' v)) '=' ((t '&' u) '&' v) or a = (t '&' (u 'or' v)) '=' ((t '&' u) 'or' (t '&' v)) or a = ('not' (t '&' u)) '=' (('not' t) 'or' ('not' u)) or a = (t '=' u) '=' (u '=' t) or a = (t '=' u) '=' (('not' t) '=' ('not' u)) ) ) ) & ( for a being object holds
( a in X2 iff ex t, u, v being GRZ-formula st
( a = 'not' (t '&' ('not' t)) or a = ('not' ('not' t)) '=' t or a = t '=' (t '&' t) or a = (t '&' u) '=' (u '&' t) or a = (t '&' (u '&' v)) '=' ((t '&' u) '&' v) or a = (t '&' (u 'or' v)) '=' ((t '&' u) 'or' (t '&' v)) or a = ('not' (t '&' u)) '=' (('not' t) 'or' ('not' u)) or a = (t '=' u) '=' (u '=' t) or a = (t '=' u) '=' (('not' t) '=' ('not' u)) ) ) ) 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