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)) );
consider X being set such that
A1: for a being object holds
( a in X iff ( a in GRZ-formula-set & S₁[a] ) ) from XBOOLE_0:sch 1();
A2: ('not' ('not' (x. 1))) '=' (x. 1) in X by A1;
X c= GRZ-formula-set by A1;
then reconsider X = X as non empty Subset of GRZ-formula-set by A2;
take X ; :: thesis: for a being object holds
( a in X 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)) ) )
thus for a being object holds
( a in X 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)) ) ) by A1; :: thesis: verum