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 S1[ Element of CQC-WFF Al] means $1 is Element of CQC-WFF Al2;
A1: S1[ VERUM Al]
proof
VERUM Al = VERUM Al2 ;
hence S1[ 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 S1[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 S1[P ! l]
let P be QC-pred_symbol of k,Al; :: thesis: for l being CQC-variable_list of k,Al holds S1[P ! l]
let l be CQC-variable_list of k,Al; :: thesis: S1[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 S1[P ! l] by A3, A4, QC_LANG1:def 12; :: thesis: verum
end;
A5: for p being Element of CQC-WFF Al st S1[p] holds
S1[ 'not' p]
proof
let p be Element of CQC-WFF Al; :: thesis: ( S1[p] implies S1[ 'not' p] )
assume S1[p] ; :: thesis: S1[ 'not' p]
then consider q being Element of CQC-WFF Al2 such that
A6: p = q ;
'not' p = 'not' q by A6;
hence S1[ 'not' p] ; :: thesis: verum
end;
A7: for p, q being Element of CQC-WFF Al st S1[p] & S1[q] holds
S1[p '&' q]
proof
let p, q be Element of CQC-WFF Al; :: thesis: ( S1[p] & S1[q] implies S1[p '&' q] )
assume ( S1[p] & S1[q] ) ; :: thesis: S1[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 S1[p '&' q] ; :: thesis: verum
end;
A9: for p being Element of CQC-WFF Al
for x being bound_QC-variable of Al st S1[p] holds
S1[ All (x,p)]
proof
let p be Element of CQC-WFF Al; :: thesis: for x being bound_QC-variable of Al st S1[p] holds
S1[ All (x,p)]
let x be bound_QC-variable of Al; :: thesis: ( S1[p] implies S1[ All (x,p)] )
assume S1[p] ; :: thesis: S1[ 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 S1[ 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
( S1[ VERUM Al] & S1[P ! l] & ( S1[r] implies S1[ 'not' r] ) & ( S1[r] & S1[s] implies S1[r '&' s] ) & ( S1[r] implies S1[ All (x,r)] ) ) by A1, A2, A5, A7, A9;
for p being Element of CQC-WFF Al holds S1[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