defpred S₁[ Element of QC-WFF ] means ( $1 is Element of CQC-WFF implies P₁[$1] );
A2: for p being Element of QC-WFF st S₁[p] holds
S₁[ 'not' p]

proof

let p be Element of QC-WFF ; :: thesis: ( S₁[p] implies S₁[ 'not' p] )
assume A3: S₁[p] ; :: thesis: S₁[ 'not' p]
assume 'not' p is Element of CQC-WFF ; :: thesis: P₁[ 'not' p]
then p is Element of CQC-WFF by Th18;
hence P₁[ 'not' p] by A1, A3; :: thesis: verum

end;

A4: for p, q being Element of QC-WFF st S₁[p] & S₁[q] holds
S₁[p '&' q]

proof

let p, q be Element of QC-WFF ; :: thesis: ( S₁[p] & S₁[q] implies S₁[p '&' q] )
assume A5: ( S₁[p] & S₁[q] ) ; :: thesis: S₁[p '&' q]
assume p '&' q is Element of CQC-WFF ; :: thesis: P₁[p '&' q]
then ( p is Element of CQC-WFF & q is Element of CQC-WFF ) by Th19;
hence P₁[p '&' q] by A1, A5; :: thesis: verum

end;

A6: for k being Element of NAT
for P being QC-pred_symbol of k
for l being QC-variable_list of k holds S₁[P ! l]

proof

let k be Element of NAT ; :: thesis: for P being QC-pred_symbol of k
for l being QC-variable_list of k holds S₁[P ! l]
let P be QC-pred_symbol of k; :: thesis: for l being QC-variable_list of k holds S₁[P ! l]
let l be QC-variable_list of k; :: thesis: S₁[P ! l]
assume A7: P ! l is Element of CQC-WFF ; :: thesis: P₁[P ! l]
then A8: { (l . j) where j is Element of NAT : ( 1 <= j & j <= len l & l . j in fixed_QC-variables ) } = {} by Th17;
{ (l . i) where i is Element of NAT : ( 1 <= i & i <= len l & l . i in free_QC-variables ) } = {} by A7, Th17;
then l is CQC-variable_list of k by A8, Th15;
hence P₁[P ! l] by A1; :: thesis: verum

end;

A9: for x being bound_QC-variable
for p being Element of QC-WFF st S₁[p] holds
S₁[ All (x,p)]

proof

let x be bound_QC-variable; :: thesis: for p being Element of QC-WFF st S₁[p] holds
S₁[ All (x,p)]
let p be Element of QC-WFF ; :: thesis: ( S₁[p] implies S₁[ All (x,p)] )
assume A10: S₁[p] ; :: thesis: S₁[ All (x,p)]
assume All (x,p) is Element of CQC-WFF ; :: thesis: P₁[ All (x,p)]
then p is Element of CQC-WFF by Th23;
hence P₁[ All (x,p)] by A1, A10; :: thesis: verum

end;

A11: S₁[ VERUM ] by A1;
for p being Element of QC-WFF holds S₁[p] from QC_LANG1:sch 1(A6, A11, A2, A4, A9);
hence for r being Element of CQC-WFF holds P₁[r] ; :: thesis: verum