let A be QC-alphabet ; for F being Element of QC-WFF A holds
( F = VERUM A or F is atomic or F is negative or F is conjunctive or F is universal )
defpred S1[ Element of QC-WFF A] means ( $1 = VERUM A or $1 is atomic or $1 is negative or $1 is conjunctive or $1 is universal );
A1:
S1[ VERUM A]
;
A2:
for p being Element of QC-WFF A st S1[p] holds
S1[ 'not' p]
by Def19;
A3:
for x being bound_QC-variable of A
for p being Element of QC-WFF A st S1[p] holds
S1[ All (x,p)]
by Def21;
A4:
for p, q being Element of QC-WFF A st S1[p] & S1[q] holds
S1[p '&' q]
by Def20;
A5:
for k being Nat
for p being QC-pred_symbol of k,A
for ll being QC-variable_list of k,A holds S1[p ! ll]
by Def18;
thus
for F being Element of QC-WFF A holds S1[F]
from QC_LANG1:sch 1(A5, A1, A2, A4, A3); verum