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