A2: now :: thesis: for x being bound_QC-variable of F1()
for p being Element of QC-WFF F1() st P1[p] holds
P1[ All (x,p)]
let x be bound_QC-variable of F1(); :: thesis: for p being Element of QC-WFF F1() st P1[p] holds
P1[ All (x,p)]
let p be Element of QC-WFF F1(); :: thesis: ( P1[p] implies P1[ All (x,p)] )
assume A3: P1[p] ; :: thesis: P1[ All (x,p)]
A4: All (x,p) is universal ;
then p = the_scope_of (All (x,p)) by Def28;
hence P1[ All (x,p)] by A1, A3, A4; :: thesis: verum
end;
A5: now :: thesis: for p being Element of QC-WFF F1() st P1[p] holds
P1[ 'not' p]
let p be Element of QC-WFF F1(); :: thesis: ( P1[p] implies P1[ 'not' p] )
assume A6: P1[p] ; :: thesis: P1[ 'not' p]
A7: 'not' p is negative ;
then p = the_argument_of ('not' p) by Def24;
hence P1[ 'not' p] by A1, A6, A7; :: thesis: verum
end;
A8: now :: thesis: for p, q being Element of QC-WFF F1() st P1[p] & P1[q] holds
P1[p '&' q]
let p, q be Element of QC-WFF F1(); :: thesis: ( P1[p] & P1[q] implies P1[p '&' q] )
assume A9: ( P1[p] & P1[q] ) ; :: thesis: P1[p '&' q]
A10: p '&' q is conjunctive ;
then ( p = the_left_argument_of (p '&' q) & q = the_right_argument_of (p '&' q) ) by Def25, Def26;
hence P1[p '&' q] by A1, A9, A10; :: thesis: verum
end;
A11: for k being Nat
for P being QC-pred_symbol of k,F1()
for ll being QC-variable_list of k,F1() holds P1[P ! ll] by A1, Def18;
A12: P1[ VERUM F1()] by A1;
thus for p being Element of QC-WFF F1() holds P1[p] from QC_LANG1:sch 1(A11, A12, A5, A8, A2); :: thesis: verum