let Al be QC-alphabet ; 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 ; 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]
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;
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;
for l being CQC-variable_list of k,Al holds S1[P ! l]let l be
CQC-variable_list of
k,
Al;
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;
verum
end;
A5:
for p being Element of CQC-WFF Al st S1[p] holds
S1[ 'not' p]
A7:
for p, q being Element of CQC-WFF Al st S1[p] & S1[q] holds
S1[p '&' q]
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)]
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
; verum