A2: now

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

end;

A3: P₁[ VERUM ] by A1;

A4: now

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

end;

A7: now

let p, q be Element of QC-WFF ; :: thesis: ( P₁[p] & P₁[q] implies P₁[p '&' q] )
assume A8: ( P₁[p] & P₁[q] ) ; :: thesis: P₁[p '&' q]
A9: 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, A8, A9; :: thesis: verum

end;

A10: 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 A11: P₁[p] ; :: thesis: P₁[ All x,p]
A12: All x,p is universal by Def20;
then p = the_scope_of (All x,p) by Def27;
hence P₁[ All x,p] by A1, A11, A12; :: thesis: verum

end;

thus for p being Element of QC-WFF holds P₁[p] from QC_LANG1:sch 1(A2, A3, A4, A7, A10); :: thesis: verum