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: for k being Element of NAT
for p being QC-pred_symbol of k
for ll being QC-variable_list of holds S₁[p ! ll] by Def17;
A2: S₁[ VERUM ] ;
A3: for p being Element of QC-WFF st S₁[p] holds
S₁[ 'not' p] by Def18;
A4: for p, q being Element of QC-WFF st S₁[p] & S₁[q] holds
S₁[p '&' q] by Def19;
A5: for x being bound_QC-variable
for p being Element of QC-WFF st S₁[p] holds
S₁[ All x,p] by Def20;
thus for F being Element of QC-WFF holds S₁[F] from QC_LANG1:sch 1(A1, A2, A3, A4, A5); :: thesis: verum