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