defpred S1[ Element of QC-WFF F1()] means ( $1 is Element of CQC-WFF F1() implies P1[$1] );
A2:
for p being Element of QC-WFF F1() st S1[p] holds
S1[ 'not' p]
A4:
for p, q being Element of QC-WFF F1() st S1[p] & S1[q] holds
S1[p '&' q]
A6:
for k being Nat
for P being QC-pred_symbol of k,F1()
for l being QC-variable_list of k,F1() holds S1[P ! l]
proof
let k be
Nat;
for P being QC-pred_symbol of k,F1()
for l being QC-variable_list of k,F1() holds S1[P ! l]let P be
QC-pred_symbol of
k,
F1();
for l being QC-variable_list of k,F1() holds S1[P ! l]let l be
QC-variable_list of
k,
F1();
S1[P ! l]
assume A7:
P ! l is
Element of
CQC-WFF F1()
;
P1[P ! l]
reconsider k =
k as
Nat ;
reconsider l =
l as
QC-variable_list of
k,
F1() ;
A8:
{ (l . j) where j is Nat : ( 1 <= j & j <= len l & l . j in fixed_QC-variables F1() ) } = {}
by Th7, A7;
{ (l . i) where i is Nat : ( 1 <= i & i <= len l & l . i in free_QC-variables F1() ) } = {}
by A7, Th7;
then
l is
CQC-variable_list of
k,
F1()
by A8, Th5;
hence
P1[
P ! l]
by A1;
verum
end;
A9:
for x being bound_QC-variable of F1()
for p being Element of QC-WFF F1() st S1[p] holds
S1[ All (x,p)]
A11:
S1[ VERUM F1()]
by A1;
for p being Element of QC-WFF F1() holds S1[p]
from QC_LANG1:sch 1(A6, A11, A2, A4, A9);
hence
for r being Element of CQC-WFF F1() holds P1[r]
; verum