let Al be QC-alphabet ; :: thesis: for p being Element of CQC-WFF Al ex Al1 being countable QC-alphabet st

( p is Element of CQC-WFF Al1 & Al is Al1 -expanding )

defpred S_{1}[ Element of CQC-WFF Al] means ex Al1 being countable QC-alphabet st

( $1 is Element of CQC-WFF Al1 & Al is Al1 -expanding );

A1: S_{1}[ VERUM Al]

for P being QC-pred_symbol of k,Al

for l being CQC-variable_list of k,Al holds S_{1}[P ! l]
_{1}[r] holds

S_{1}[ 'not' r]
_{1}[r] & S_{1}[s] holds

S_{1}[r '&' s]

for r being Element of CQC-WFF Al st S_{1}[r] holds

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

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, A15, A19;

for p being Element of CQC-WFF Al holds S_{1}[p]
from CQC_LANG:sch 1(A32);

hence for p being Element of CQC-WFF Al ex Al1 being countable QC-alphabet st

( p is Element of CQC-WFF Al1 & Al is Al1 -expanding ) ; :: thesis: verum

( p is Element of CQC-WFF Al1 & Al is Al1 -expanding )

defpred S

( $1 is Element of CQC-WFF Al1 & Al is Al1 -expanding );

A1: S

proof

A2:
for k being Nat
set Al1 = [:NAT,NAT:];

reconsider Al1 = [:NAT,NAT:] as countable QC-alphabet by QC_LANG1:def 1, CARD_4:7;

( NAT c= QC-symbols Al & Al = [:NAT,(QC-symbols Al):] ) by QC_LANG1:3, QC_LANG1:5;

then Al1 c= Al by ZFMISC_1:95;

then reconsider Al = Al as Al1 -expanding QC-alphabet by Def1;

VERUM Al1 = VERUM Al ;

hence S_{1}[ VERUM Al]
; :: thesis: verum

end;reconsider Al1 = [:NAT,NAT:] as countable QC-alphabet by QC_LANG1:def 1, CARD_4:7;

( NAT c= QC-symbols Al & Al = [:NAT,(QC-symbols Al):] ) by QC_LANG1:3, QC_LANG1:5;

then Al1 c= Al by ZFMISC_1:95;

then reconsider Al = Al as Al1 -expanding QC-alphabet by Def1;

VERUM Al1 = VERUM Al ;

hence S

for P being QC-pred_symbol of k,Al

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

proof

A15:
for r 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]

( bound_QC-variables Al c= QC-variables Al & QC-variables Al c= [:NAT,(QC-symbols Al):] ) by QC_LANG1:4;

then bound_QC-variables Al c= [:NAT,(QC-symbols Al):] ;

then consider A, B being set such that

A3: ( A is finite & A c= NAT & B is finite & B c= QC-symbols Al & rng l c= [:A,B:] ) by FINSET_1:13, XBOOLE_1:1;

[:A,B:] c= [:NAT,B:] by A3, ZFMISC_1:95;

then A4: rng l c= [:NAT,B:] by A3;

set Al1 = ([:NAT,NAT:] \/ [:NAT,{(P `2)}:]) \/ [:NAT,B:];

( [:NAT,NAT:] is countable & [:NAT,{(P `2)}:] is countable ) by CARD_4:7;

then A5: ( [:NAT,NAT:] \/ [:NAT,{(P `2)}:] is countable & [:NAT,B:] is countable ) by A3, CARD_2:85, CARD_4:7;

A6: ([:NAT,NAT:] \/ [:NAT,{(P `2)}:]) \/ [:NAT,B:] = [:NAT,(NAT \/ {(P `2)}):] \/ [:NAT,B:] by ZFMISC_1:97

.= [:NAT,((NAT \/ {(P `2)}) \/ B):] by ZFMISC_1:97 ;

( NAT c= NAT \/ {(P `2)} & NAT \/ {(P `2)} c= (NAT \/ {(P `2)}) \/ B ) by XBOOLE_1:7;

then reconsider Al1 = ([:NAT,NAT:] \/ [:NAT,{(P `2)}:]) \/ [:NAT,B:] as countable QC-alphabet by A5, A6, QC_LANG1:def 1, CARD_2:85, XBOOLE_1:1;

P in [:NAT,(QC-symbols Al):] by TARSKI:def 3, QC_LANG1:6;

then consider a, b being object such that

A7: ( a in NAT & b in QC-symbols Al & P = [a,b] ) by ZFMISC_1:def 2;

P `2 in QC-symbols Al by A7;

then ( {(P `2)} c= QC-symbols Al & NAT c= NAT & NAT c= QC-symbols Al ) by QC_LANG1:3, ZFMISC_1:31;

then ( [:NAT,{(P `2)}:] c= [:NAT,(QC-symbols Al):] & [:NAT,NAT:] c= [:NAT,(QC-symbols Al):] ) by ZFMISC_1:95;

then ( [:NAT,NAT:] \/ [:NAT,{(P `2)}:] c= [:NAT,(QC-symbols Al):] & [:NAT,B:] c= [:NAT,(QC-symbols Al):] ) by A3, ZFMISC_1:95, XBOOLE_1:8;

then Al1 c= [:NAT,(QC-symbols Al):] by XBOOLE_1:8;

then Al1 c= Al by QC_LANG1:5;

then reconsider Al = Al as Al1 -expanding QC-alphabet by Def1;

[:NAT,((NAT \/ {(P `2)}) \/ B):] = [:NAT,(QC-symbols Al1):] by A6, QC_LANG1:5;

then A8: QC-symbols Al1 = (NAT \/ {(P `2)}) \/ B by ZFMISC_1:110;

set P2 = [a,b];

b = P `2 by A7;

then b in {(P `2)} by TARSKI:def 1;

then b in NAT \/ {(P `2)} by XBOOLE_0:def 3;

then reconsider b = b as QC-symbol of Al1 by A8, XBOOLE_0:def 3;

reconsider a = a as Element of NAT by A7;

A9: ( P `1 = 7 + (the_arity_of P) & P `1 = a ) by A7, QC_LANG1:def 8;

then 7 <= a by NAT_1:11;

then [a,b] in { [n,x] where n is Nat, x is QC-symbol of Al1 : 7 <= n } ;

then reconsider P2 = [a,b] as QC-pred_symbol of Al1 ;

P2 `1 = 7 + k by A9, QC_LANG1:11;

then the_arity_of P2 = k by QC_LANG1:def 8;

then P2 in { Q where Q is QC-pred_symbol of Al1 : the_arity_of Q = k } ;

then reconsider P2 = P2 as QC-pred_symbol of k,Al1 ;

set l2 = l;

for s being object st s in rng l holds

s in bound_QC-variables Al1

reconsider l2 = l as CQC-variable_list of k,Al1 by A14, FINSEQ_1:def 4, XBOOLE_1:1;

P2 ! l2 = Al -Cast (P2 ! l2)

.= (Al -Cast P2) ! (Al -Cast l2) by Th8

.= P ! l by A7 ;

then ( P ! l is Element of CQC-WFF Al1 & Al is Al1 -expanding ) ;

hence S_{1}[P ! l]
; :: 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

( bound_QC-variables Al c= QC-variables Al & QC-variables Al c= [:NAT,(QC-symbols Al):] ) by QC_LANG1:4;

then bound_QC-variables Al c= [:NAT,(QC-symbols Al):] ;

then consider A, B being set such that

A3: ( A is finite & A c= NAT & B is finite & B c= QC-symbols Al & rng l c= [:A,B:] ) by FINSET_1:13, XBOOLE_1:1;

[:A,B:] c= [:NAT,B:] by A3, ZFMISC_1:95;

then A4: rng l c= [:NAT,B:] by A3;

set Al1 = ([:NAT,NAT:] \/ [:NAT,{(P `2)}:]) \/ [:NAT,B:];

( [:NAT,NAT:] is countable & [:NAT,{(P `2)}:] is countable ) by CARD_4:7;

then A5: ( [:NAT,NAT:] \/ [:NAT,{(P `2)}:] is countable & [:NAT,B:] is countable ) by A3, CARD_2:85, CARD_4:7;

A6: ([:NAT,NAT:] \/ [:NAT,{(P `2)}:]) \/ [:NAT,B:] = [:NAT,(NAT \/ {(P `2)}):] \/ [:NAT,B:] by ZFMISC_1:97

.= [:NAT,((NAT \/ {(P `2)}) \/ B):] by ZFMISC_1:97 ;

( NAT c= NAT \/ {(P `2)} & NAT \/ {(P `2)} c= (NAT \/ {(P `2)}) \/ B ) by XBOOLE_1:7;

then reconsider Al1 = ([:NAT,NAT:] \/ [:NAT,{(P `2)}:]) \/ [:NAT,B:] as countable QC-alphabet by A5, A6, QC_LANG1:def 1, CARD_2:85, XBOOLE_1:1;

P in [:NAT,(QC-symbols Al):] by TARSKI:def 3, QC_LANG1:6;

then consider a, b being object such that

A7: ( a in NAT & b in QC-symbols Al & P = [a,b] ) by ZFMISC_1:def 2;

P `2 in QC-symbols Al by A7;

then ( {(P `2)} c= QC-symbols Al & NAT c= NAT & NAT c= QC-symbols Al ) by QC_LANG1:3, ZFMISC_1:31;

then ( [:NAT,{(P `2)}:] c= [:NAT,(QC-symbols Al):] & [:NAT,NAT:] c= [:NAT,(QC-symbols Al):] ) by ZFMISC_1:95;

then ( [:NAT,NAT:] \/ [:NAT,{(P `2)}:] c= [:NAT,(QC-symbols Al):] & [:NAT,B:] c= [:NAT,(QC-symbols Al):] ) by A3, ZFMISC_1:95, XBOOLE_1:8;

then Al1 c= [:NAT,(QC-symbols Al):] by XBOOLE_1:8;

then Al1 c= Al by QC_LANG1:5;

then reconsider Al = Al as Al1 -expanding QC-alphabet by Def1;

[:NAT,((NAT \/ {(P `2)}) \/ B):] = [:NAT,(QC-symbols Al1):] by A6, QC_LANG1:5;

then A8: QC-symbols Al1 = (NAT \/ {(P `2)}) \/ B by ZFMISC_1:110;

set P2 = [a,b];

b = P `2 by A7;

then b in {(P `2)} by TARSKI:def 1;

then b in NAT \/ {(P `2)} by XBOOLE_0:def 3;

then reconsider b = b as QC-symbol of Al1 by A8, XBOOLE_0:def 3;

reconsider a = a as Element of NAT by A7;

A9: ( P `1 = 7 + (the_arity_of P) & P `1 = a ) by A7, QC_LANG1:def 8;

then 7 <= a by NAT_1:11;

then [a,b] in { [n,x] where n is Nat, x is QC-symbol of Al1 : 7 <= n } ;

then reconsider P2 = [a,b] as QC-pred_symbol of Al1 ;

P2 `1 = 7 + k by A9, QC_LANG1:11;

then the_arity_of P2 = k by QC_LANG1:def 8;

then P2 in { Q where Q is QC-pred_symbol of Al1 : the_arity_of Q = k } ;

then reconsider P2 = P2 as QC-pred_symbol of k,Al1 ;

set l2 = l;

for s being object st s in rng l holds

s in bound_QC-variables Al1

proof

then A14:
rng l c= bound_QC-variables Al1
;
let s be object ; :: thesis: ( s in rng l implies s in bound_QC-variables Al1 )

assume A10: s in rng l ; :: thesis: s in bound_QC-variables Al1

consider s1, s2 being object such that

A11: ( s1 in {4} & s2 in QC-symbols Al & s = [s1,s2] ) by A10, ZFMISC_1:def 2;

B c= QC-symbols Al1 by A8, XBOOLE_1:7;

then A12: [:NAT,B:] c= [:NAT,(QC-symbols Al1):] by ZFMISC_1:95;

s in [:NAT,B:] by A4, A10;

then consider s3, s4 being object such that

A13: ( s3 in NAT & s4 in QC-symbols Al1 & s = [s3,s4] ) by A12, ZFMISC_1:def 2;

s = [s1,s4] by A11, A13, XTUPLE_0:1;

hence s in bound_QC-variables Al1 by A11, A13, ZFMISC_1:def 2; :: thesis: verum

end;assume A10: s in rng l ; :: thesis: s in bound_QC-variables Al1

consider s1, s2 being object such that

A11: ( s1 in {4} & s2 in QC-symbols Al & s = [s1,s2] ) by A10, ZFMISC_1:def 2;

B c= QC-symbols Al1 by A8, XBOOLE_1:7;

then A12: [:NAT,B:] c= [:NAT,(QC-symbols Al1):] by ZFMISC_1:95;

s in [:NAT,B:] by A4, A10;

then consider s3, s4 being object such that

A13: ( s3 in NAT & s4 in QC-symbols Al1 & s = [s3,s4] ) by A12, ZFMISC_1:def 2;

s = [s1,s4] by A11, A13, XTUPLE_0:1;

hence s in bound_QC-variables Al1 by A11, A13, ZFMISC_1:def 2; :: thesis: verum

reconsider l2 = l as CQC-variable_list of k,Al1 by A14, FINSEQ_1:def 4, XBOOLE_1:1;

P2 ! l2 = Al -Cast (P2 ! l2)

.= (Al -Cast P2) ! (Al -Cast l2) by Th8

.= P ! l by A7 ;

then ( P ! l is Element of CQC-WFF Al1 & Al is Al1 -expanding ) ;

hence S

S

proof

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

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

consider Al1 being countable QC-alphabet such that

A17: ( r is Element of CQC-WFF Al1 & Al is Al1 -expanding ) by A16;

reconsider Al = Al as Al1 -expanding QC-alphabet by A17;

consider r2 being Element of CQC-WFF Al1 such that

A18: r = r2 by A17;

'not' r2 = 'not' r by A18;

hence S_{1}[ 'not' r]
by A17; :: thesis: verum

end;assume A16: S

consider Al1 being countable QC-alphabet such that

A17: ( r is Element of CQC-WFF Al1 & Al is Al1 -expanding ) by A16;

reconsider Al = Al as Al1 -expanding QC-alphabet by A17;

consider r2 being Element of CQC-WFF Al1 such that

A18: r = r2 by A17;

'not' r2 = 'not' r by A18;

hence S

S

proof

for x being bound_QC-variable of Al
let r, s be Element of CQC-WFF Al; :: thesis: ( S_{1}[r] & S_{1}[s] implies S_{1}[r '&' s] )

assume A20: ( S_{1}[r] & S_{1}[s] )
; :: thesis: S_{1}[r '&' s]

consider Al1, Al2 being countable QC-alphabet such that

A21: ( r is Element of CQC-WFF Al1 & s is Element of CQC-WFF Al2 & Al is Al1 -expanding & Al is Al2 -expanding ) by A20;

set Al3 = Al1 \/ Al2;

( Al1 = [:NAT,(QC-symbols Al1):] & Al2 = [:NAT,(QC-symbols Al2):] ) by QC_LANG1:5;

then A22: Al1 \/ Al2 = [:NAT,((QC-symbols Al1) \/ (QC-symbols Al2)):] by ZFMISC_1:97;

NAT c= (QC-symbols Al1) \/ (QC-symbols Al2) by XBOOLE_1:10, QC_LANG1:3;

then reconsider Al3 = Al1 \/ Al2 as QC-alphabet by A22, QC_LANG1:def 1;

reconsider Al3 = Al3 as countable Al1 -expanding Al2 -expanding QC-alphabet by Def1, CARD_2:85, XBOOLE_1:7;

consider r2 being Element of CQC-WFF Al1, s2 being Element of CQC-WFF Al2 such that

A23: ( r2 = r & s2 = s ) by A21;

reconsider r2 = r2 as Element of CQC-WFF Al3 by Th7;

reconsider s2 = s2 as Element of CQC-WFF Al3 by Th7;

( Al1 c= Al & Al2 c= Al ) by A21;

then reconsider Al = Al as Al3 -expanding QC-alphabet by Def1, XBOOLE_1:8;

r2 '&' s2 = r '&' s by A23;

then ( r '&' s is Element of CQC-WFF Al3 & Al is Al3 -expanding ) ;

hence S_{1}[r '&' s]
; :: thesis: verum

end;assume A20: ( S

consider Al1, Al2 being countable QC-alphabet such that

A21: ( r is Element of CQC-WFF Al1 & s is Element of CQC-WFF Al2 & Al is Al1 -expanding & Al is Al2 -expanding ) by A20;

set Al3 = Al1 \/ Al2;

( Al1 = [:NAT,(QC-symbols Al1):] & Al2 = [:NAT,(QC-symbols Al2):] ) by QC_LANG1:5;

then A22: Al1 \/ Al2 = [:NAT,((QC-symbols Al1) \/ (QC-symbols Al2)):] by ZFMISC_1:97;

NAT c= (QC-symbols Al1) \/ (QC-symbols Al2) by XBOOLE_1:10, QC_LANG1:3;

then reconsider Al3 = Al1 \/ Al2 as QC-alphabet by A22, QC_LANG1:def 1;

reconsider Al3 = Al3 as countable Al1 -expanding Al2 -expanding QC-alphabet by Def1, CARD_2:85, XBOOLE_1:7;

consider r2 being Element of CQC-WFF Al1, s2 being Element of CQC-WFF Al2 such that

A23: ( r2 = r & s2 = s ) by A21;

reconsider r2 = r2 as Element of CQC-WFF Al3 by Th7;

reconsider s2 = s2 as Element of CQC-WFF Al3 by Th7;

( Al1 c= Al & Al2 c= Al ) by A21;

then reconsider Al = Al as Al3 -expanding QC-alphabet by Def1, XBOOLE_1:8;

r2 '&' s2 = r '&' s by A23;

then ( r '&' s is Element of CQC-WFF Al3 & Al is Al3 -expanding ) ;

hence S

for r being Element of CQC-WFF Al st S

S

proof

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

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

let r be Element of CQC-WFF Al; :: thesis: ( S_{1}[r] implies S_{1}[ All (x,r)] )

assume A24: S_{1}[r]
; :: thesis: S_{1}[ All (x,r)]

consider Al1 being countable QC-alphabet such that

A25: ( r is Element of CQC-WFF Al1 & Al is Al1 -expanding ) by A24;

consider s1, s2 being object such that

A26: ( s1 in {4} & s2 in QC-symbols Al & x = [s1,s2] ) by ZFMISC_1:def 2;

set Al2 = [:NAT,((QC-symbols Al1) \/ {s2}):];

A27: ( Al1 = [:NAT,(QC-symbols Al1):] & QC-symbols Al1 c= (QC-symbols Al1) \/ {s2} & NAT c= QC-symbols Al1 ) by QC_LANG1:3, QC_LANG1:5, XBOOLE_1:7;

then ( Al1 c= [:NAT,((QC-symbols Al1) \/ {s2}):] & NAT c= (QC-symbols Al1) \/ {s2} ) by ZFMISC_1:95;

then reconsider Al2 = [:NAT,((QC-symbols Al1) \/ {s2}):] as Al1 -expanding QC-alphabet by Def1, QC_LANG1:def 1;

A28: ( Al2 = [:NAT,(QC-symbols Al1):] \/ [:NAT,{s2}:] & [:NAT,(QC-symbols Al1):] c= Al ) by A25, A27, ZFMISC_1:97;

( [:NAT,(QC-symbols Al1):] is countable & [:NAT,{s2}:] is countable ) by QC_LANG1:5, CARD_4:7;

then reconsider Al2 = Al2 as countable Al1 -expanding QC-alphabet by A28, CARD_2:85;

{s2} c= QC-symbols Al by A26, ZFMISC_1:31;

then ( [:NAT,{s2}:] c= [:NAT,(QC-symbols Al):] & Al = [:NAT,(QC-symbols Al):] ) by QC_LANG1:5, ZFMISC_1:96;

then reconsider Al = Al as Al2 -expanding QC-alphabet by Def1, A28, XBOOLE_1:8;

consider r2 being Element of CQC-WFF Al1 such that

A29: r = r2 by A25;

reconsider r2 = r2 as Element of CQC-WFF Al2 by Th7;

A30: x = [4,s2] by A26, TARSKI:def 1;

Al2 = [:NAT,(QC-symbols Al2):] by QC_LANG1:5;

then ( QC-symbols Al2 = (QC-symbols Al1) \/ {s2} & s2 in {s2} ) by TARSKI:def 1, ZFMISC_1:110;

then s2 in QC-symbols Al2 by XBOOLE_0:def 3;

then x is bound_QC-variable of Al2 by A30, ZFMISC_1:105;

then consider x2 being bound_QC-variable of Al2 such that

A31: x = x2 ;

All (x2,r2) = All (x,r) by A29, A31;

then ( All (x,r) is Element of CQC-WFF Al2 & Al is Al2 -expanding ) ;

hence S_{1}[ All (x,r)]
; :: thesis: verum

end;S

let r be Element of CQC-WFF Al; :: thesis: ( S

assume A24: S

consider Al1 being countable QC-alphabet such that

A25: ( r is Element of CQC-WFF Al1 & Al is Al1 -expanding ) by A24;

consider s1, s2 being object such that

A26: ( s1 in {4} & s2 in QC-symbols Al & x = [s1,s2] ) by ZFMISC_1:def 2;

set Al2 = [:NAT,((QC-symbols Al1) \/ {s2}):];

A27: ( Al1 = [:NAT,(QC-symbols Al1):] & QC-symbols Al1 c= (QC-symbols Al1) \/ {s2} & NAT c= QC-symbols Al1 ) by QC_LANG1:3, QC_LANG1:5, XBOOLE_1:7;

then ( Al1 c= [:NAT,((QC-symbols Al1) \/ {s2}):] & NAT c= (QC-symbols Al1) \/ {s2} ) by ZFMISC_1:95;

then reconsider Al2 = [:NAT,((QC-symbols Al1) \/ {s2}):] as Al1 -expanding QC-alphabet by Def1, QC_LANG1:def 1;

A28: ( Al2 = [:NAT,(QC-symbols Al1):] \/ [:NAT,{s2}:] & [:NAT,(QC-symbols Al1):] c= Al ) by A25, A27, ZFMISC_1:97;

( [:NAT,(QC-symbols Al1):] is countable & [:NAT,{s2}:] is countable ) by QC_LANG1:5, CARD_4:7;

then reconsider Al2 = Al2 as countable Al1 -expanding QC-alphabet by A28, CARD_2:85;

{s2} c= QC-symbols Al by A26, ZFMISC_1:31;

then ( [:NAT,{s2}:] c= [:NAT,(QC-symbols Al):] & Al = [:NAT,(QC-symbols Al):] ) by QC_LANG1:5, ZFMISC_1:96;

then reconsider Al = Al as Al2 -expanding QC-alphabet by Def1, A28, XBOOLE_1:8;

consider r2 being Element of CQC-WFF Al1 such that

A29: r = r2 by A25;

reconsider r2 = r2 as Element of CQC-WFF Al2 by Th7;

A30: x = [4,s2] by A26, TARSKI:def 1;

Al2 = [:NAT,(QC-symbols Al2):] by QC_LANG1:5;

then ( QC-symbols Al2 = (QC-symbols Al1) \/ {s2} & s2 in {s2} ) by TARSKI:def 1, ZFMISC_1:110;

then s2 in QC-symbols Al2 by XBOOLE_0:def 3;

then x is bound_QC-variable of Al2 by A30, ZFMISC_1:105;

then consider x2 being bound_QC-variable of Al2 such that

A31: x = x2 ;

All (x2,r2) = All (x,r) by A29, A31;

then ( All (x,r) is Element of CQC-WFF Al2 & Al is Al2 -expanding ) ;

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 ex Al1 being countable QC-alphabet st

( p is Element of CQC-WFF Al1 & Al is Al1 -expanding ) ; :: thesis: verum