defpred S₁[ set ] means $1 is FinSequence of CQC-WFF ;
consider X being set such that
A1: for a being set holds
( a in X iff ( a in bool [:NAT ,CQC-WFF :] & S₁[a] ) ) from XBOOLE_0:sch 1();
take X ; :: thesis: for a being set holds
( a in X iff a is FinSequence of CQC-WFF )
thus for a being set holds
( a in X iff a is FinSequence of CQC-WFF ) by A1; :: thesis: verum