A2: now

let x be bound_QC-variable; :: thesis: for p being Element of QC-WFF st P₁[p] holds
P₁[ All (x,p)]
let p be Element of QC-WFF ; :: thesis: ( P₁[p] implies P₁[ All (x,p)] )
assume A3: P₁[p] ; :: thesis: P₁[ All (x,p)]
A4: All (x,p) is universal by Def20;
then p = the_scope_of (All (x,p)) by Def27;
hence P₁[ All (x,p)] by A1, A3, A4; :: thesis: verum

end;

A5: now

let p be Element of QC-WFF ; :: thesis: ( P₁[p] implies P₁[ 'not' p] )
assume A6: P₁[p] ; :: thesis: P₁[ 'not' p]
A7: 'not' p is negative by Def18;
then p = the_argument_of ('not' p) by Def23;
hence P₁[ 'not' p] by A1, A6, A7; :: thesis: verum

end;

A8: now

let p, q be Element of QC-WFF ; :: thesis: ( P₁[p] & P₁[q] implies P₁[p '&' q] )
assume A9: ( P₁[p] & P₁[q] ) ; :: thesis: P₁[p '&' q]
A10: p '&' q is conjunctive by Def19;
then ( p = the_left_argument_of (p '&' q) & q = the_right_argument_of (p '&' q) ) by Def24, Def25;
hence P₁[p '&' q] by A1, A9, A10; :: thesis: verum

end;

A11: now

let k be Element of NAT ; :: thesis: for P being QC-pred_symbol of k
for ll being QC-variable_list of k holds P₁[P ! ll]
let P be QC-pred_symbol of k; :: thesis: for ll being QC-variable_list of k holds P₁[P ! ll]
let ll be QC-variable_list of k; :: thesis: P₁[P ! ll]
P ! ll is atomic by Def17;
hence P₁[P ! ll] by A1; :: thesis: verum

end;

A12: P₁[ VERUM ] by A1;
thus for p being Element of QC-WFF holds P₁[p] from QC_LANG1:sch 1(A11, A12, A5, A8, A2); :: thesis: verum