let Al be QC-alphabet ; :: thesis: for Al2 being Al -expanding QC-alphabet
for p being Element of CQC-WFF Al holds p is Element of CQC-WFF Al2
let Al2 be Al -expanding QC-alphabet ; :: thesis: for p being Element of CQC-WFF Al holds p is Element of CQC-WFF Al2
defpred S₁[ Element of CQC-WFF Al] means $1 is Element of CQC-WFF Al2;
A1: S₁[ VERUM Al]

proof

VERUM Al = VERUM Al2 ;
hence S₁[ VERUM Al] ; :: thesis: verum

end;

A2: for k being Nat
for P being QC-pred_symbol of k,Al
for l being CQC-variable_list of k,Al holds S₁[P ! l]

proof

let k be Nat; :: thesis: for P being QC-pred_symbol of k,Al
for l being CQC-variable_list of k,Al holds S₁[P ! l]
let P be QC-pred_symbol of k,Al; :: thesis: for l being CQC-variable_list of k,Al holds S₁[P ! l]
let l be CQC-variable_list of k,Al; :: thesis: S₁[P ! l]
A3: the_arity_of P = len l by Th1;
( P is QC-pred_symbol of k,Al2 & l is CQC-variable_list of k,Al2 ) by Th5, Th6;
then consider P2 being QC-pred_symbol of k,Al2, l2 being CQC-variable_list of k,Al2 such that
A4: ( P = P2 & l = l2 ) ;
the_arity_of P2 = len l2 by Th1;
then P2 ! l2 = <*P2*> ^ l2 by QC_LANG1:def 12;
hence S₁[P ! l] by A3, A4, QC_LANG1:def 12; :: thesis: verum

end;

A5: for p being Element of CQC-WFF Al st S₁[p] holds
S₁[ 'not' p]

proof

let p be Element of CQC-WFF Al; :: thesis: ( S₁[p] implies S₁[ 'not' p] )
assume S₁[p] ; :: thesis: S₁[ 'not' p]
then consider q being Element of CQC-WFF Al2 such that
A6: p = q ;
'not' p = 'not' q by A6;
hence S₁[ 'not' p] ; :: thesis: verum

end;

A7: for p, q being Element of CQC-WFF Al st S₁[p] & S₁[q] holds
S₁[p '&' q]

proof

let p, q be Element of CQC-WFF Al; :: thesis: ( S₁[p] & S₁[q] implies S₁[p '&' q] )
assume ( S₁[p] & S₁[q] ) ; :: thesis: S₁[p '&' q]
then consider t, u being Element of CQC-WFF Al2 such that
A8: ( p = t & q = u ) ;
p '&' q = t '&' u by A8;
hence S₁[p '&' q] ; :: thesis: verum

end;

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

proof

let p be Element of CQC-WFF Al; :: thesis: for x being bound_QC-variable of Al st S₁[p] holds
S₁[ All (x,p)]
let x be bound_QC-variable of Al; :: thesis: ( S₁[p] implies S₁[ All (x,p)] )
assume S₁[p] ; :: thesis: S₁[ All (x,p)]
then consider q being Element of CQC-WFF Al2 such that
A10: p = q ;
x is bound_QC-variable of Al2 by Th4, TARSKI:def 3;
then consider y being bound_QC-variable of Al2 such that
A11: x = y ;
All (x,p) = All (y,q) by A10, A11;
hence S₁[ All (x,p)] ; :: thesis: verum

end;

A12: for r, s being Element of CQC-WFF Al
for x being bound_QC-variable of Al
for k being Nat
for l being CQC-variable_list of k,Al
for P being QC-pred_symbol of k,Al holds
( S₁[ VERUM Al] & S₁[P ! l] & ( S₁[r] implies S₁[ 'not' r] ) & ( S₁[r] & S₁[s] implies S₁[r '&' s] ) & ( S₁[r] implies S₁[ All (x,r)] ) ) by A1, A2, A5, A7, A9;
for p being Element of CQC-WFF Al holds S₁[p] from CQC_LANG:sch 1(A12);
hence for p being Element of CQC-WFF Al holds p is Element of CQC-WFF Al2 ; :: thesis: verum