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)) );
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: ((x. 1) '=' (x. 1)) => (((x. 1) '&' (x. 1)) '=' ((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 = (t '=' u) => ((t '&' v) '=' (u '&' v)) or a = (t '=' u) => ((t 'or' v) '=' (u 'or' v)) or a = (t '=' u) => ((t '=' v) '=' (u '=' v)) ) )
thus for a being object holds
( a in X 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)) ) ) by A1; :: thesis: verum