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_{1}[ Element of CQC-WFF Al] means $1 is Element of CQC-WFF Al2;

A1: S_{1}[ 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 S_{1}[P ! l]
_{1}[p] holds

S_{1}[ 'not' p]
_{1}[p] & S_{1}[q] holds

S_{1}[p '&' q]

for x being bound_QC-variable of Al st S_{1}[p] holds

S_{1}[ All (x,p)]

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_{1}[ VERUM Al] & S_{1}[P ! l] & ( S_{1}[r] implies S_{1}[ 'not' r] ) & ( S_{1}[r] & S_{1}[s] implies S_{1}[r '&' s] ) & ( S_{1}[r] implies S_{1}[ All (x,r)] ) )
by A1, A2, A5, A7, A9;

for p being Element of CQC-WFF Al holds S_{1}[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

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

A1: S

for P being QC-pred_symbol of k,Al

for l being CQC-variable_list of k,Al holds S

proof

A5:
for p being Element of CQC-WFF Al st S
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_{1}[P ! l]

let P be QC-pred_symbol of k,Al; :: thesis: for l being CQC-variable_list of k,Al holds S_{1}[P ! l]

let l be CQC-variable_list of k,Al; :: thesis: S_{1}[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_{1}[P ! l]
by A3, A4, QC_LANG1:def 12; :: thesis: verum

end;for l being CQC-variable_list of k,Al holds S

let P be QC-pred_symbol of k,Al; :: thesis: for l being CQC-variable_list of k,Al holds S

let l be CQC-variable_list of k,Al; :: thesis: S

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

S

proof

A7:
for p, q being Element of CQC-WFF Al st S
let p be Element of CQC-WFF Al; :: thesis: ( S_{1}[p] implies S_{1}[ 'not' p] )

assume S_{1}[p]
; :: thesis: S_{1}[ 'not' p]

then consider q being Element of CQC-WFF Al2 such that

A6: p = q ;

'not' p = 'not' q by A6;

hence S_{1}[ 'not' p]
; :: thesis: verum

end;assume S

then consider q being Element of CQC-WFF Al2 such that

A6: p = q ;

'not' p = 'not' q by A6;

hence S

S

proof

A9:
for p being Element of CQC-WFF Al
let p, q be Element of CQC-WFF Al; :: thesis: ( S_{1}[p] & S_{1}[q] implies S_{1}[p '&' q] )

assume ( S_{1}[p] & S_{1}[q] )
; :: thesis: S_{1}[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_{1}[p '&' q]
; :: thesis: verum

end;assume ( S

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

for x being bound_QC-variable of Al st S

S

proof

A12:
for r, s being Element of CQC-WFF Al
let p be Element of CQC-WFF Al; :: thesis: for x being bound_QC-variable of Al st S_{1}[p] holds

S_{1}[ All (x,p)]

let x be bound_QC-variable of Al; :: thesis: ( S_{1}[p] implies S_{1}[ All (x,p)] )

assume S_{1}[p]
; :: thesis: S_{1}[ 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_{1}[ All (x,p)]
; :: thesis: verum

end;S

let x be bound_QC-variable of Al; :: thesis: ( S

assume S

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

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

for p being Element of CQC-WFF Al holds S

hence for p being Element of CQC-WFF Al holds p is Element of CQC-WFF Al2 ; :: thesis: verum