defpred S_{1}[ 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_{1}[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

consider X being set such that

A1: for a being object holds

( a in X iff ( a in bool [:NAT,(CQC-WFF Al):] & S

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