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 S1[ 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: S1[ VERUM Al]
proof
set Al1 = ;
reconsider Al1 = as countable QC-alphabet by ;
( NAT c= QC-symbols Al & Al = [:NAT,():] ) by ;
then Al1 c= Al by ZFMISC_1:95;
then reconsider Al = Al as Al1 -expanding QC-alphabet by Def1;
VERUM Al1 = VERUM Al ;
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]
( bound_QC-variables Al c= QC-variables Al & QC-variables Al c= [:NAT,():] ) by QC_LANG1:4;
then bound_QC-variables Al c= [:NAT,():] ;
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 ;
[:A,B:] c= [:NAT,B:] by ;
then A4: rng l c= [:NAT,B:] by A3;
set Al1 = ( \/ [:NAT,{(P `2)}:]) \/ [:NAT,B:];
( [::] is countable & [:NAT,{(P `2)}:] is countable ) by CARD_4:7;
then A5: ( [::] \/ [:NAT,{(P `2)}:] is countable & [:NAT,B:] is countable ) by ;
A6: ( \/ [: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,{(P `2)}:]) \/ [:NAT,B:] as countable QC-alphabet by ;
P in [:NAT,():] by ;
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 ;
then ( [:NAT,{(P `2)}:] c= [:NAT,():] & c= [:NAT,():] ) by ZFMISC_1:95;
then ( [::] \/ [:NAT,{(P `2)}:] c= [:NAT,():] & [:NAT,B:] c= [:NAT,():] ) by ;
then Al1 c= [:NAT,():] 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 ;
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 ;
reconsider a = a as Element of NAT by A7;
A9: ( P `1 = 7 + () & P `1 = a ) by ;
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 ;
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
let s be object ; :: thesis: ( s in rng l implies s in bound_QC-variables Al1 )
assume A10: s in rng l ; :: thesis:
consider s1, s2 being object such that
A11: ( s1 in {4} & s2 in QC-symbols Al & s = [s1,s2] ) by ;
B c= QC-symbols Al1 by ;
then A12: [:NAT,B:] c= [:NAT,(QC-symbols Al1):] by ZFMISC_1:95;
s in [:NAT,B:] by ;
then consider s3, s4 being object such that
A13: ( s3 in NAT & s4 in QC-symbols Al1 & s = [s3,s4] ) by ;
s = [s1,s4] by ;
hence s in bound_QC-variables Al1 by ; :: thesis: verum
end;
then A14: rng l c= bound_QC-variables Al1 ;
reconsider l2 = l as CQC-variable_list of k,Al1 by ;
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 S1[P ! l] ; :: thesis: verum
end;
A15: for r being Element of CQC-WFF Al st S1[r] holds
S1[ 'not' r]
proof
let r be Element of CQC-WFF Al; :: thesis: ( S1[r] implies S1[ 'not' r] )
assume A16: S1[r] ; :: thesis: S1[ '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 S1[ 'not' r] by A17; :: thesis: verum
end;
A19: for r, s being Element of CQC-WFF Al st S1[r] & S1[s] holds
S1[r '&' s]
proof
let r, s be Element of CQC-WFF Al; :: thesis: ( S1[r] & S1[s] implies S1[r '&' s] )
assume A20: ( S1[r] & S1[s] ) ; :: thesis: S1[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 ;
then reconsider Al3 = Al1 \/ Al2 as QC-alphabet by ;
reconsider Al3 = Al3 as countable Al1 -expanding Al2 -expanding QC-alphabet by ;
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 ;
r2 '&' s2 = r '&' s by A23;
then ( r '&' s is Element of CQC-WFF Al3 & Al is Al3 -expanding ) ;
hence S1[r '&' s] ; :: thesis: verum
end;
for x being bound_QC-variable of Al
for r being Element of CQC-WFF Al st S1[r] holds
S1[ All (x,r)]
proof
let x be bound_QC-variable of Al; :: thesis: for r being Element of CQC-WFF Al st S1[r] holds
S1[ All (x,r)]

let r be Element of CQC-WFF Al; :: thesis: ( S1[r] implies S1[ All (x,r)] )
assume A24: S1[r] ; :: thesis: S1[ 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 ;
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 ;
A28: ( Al2 = [:NAT,(QC-symbols Al1):] \/ [:NAT,{s2}:] & [:NAT,(QC-symbols Al1):] c= Al ) by ;
( [:NAT,(QC-symbols Al1):] is countable & [:NAT,{s2}:] is countable ) by ;
then reconsider Al2 = Al2 as countable Al1 -expanding QC-alphabet by ;
{s2} c= QC-symbols Al by ;
then ( [:NAT,{s2}:] c= [:NAT,():] & Al = [:NAT,():] ) by ;
then reconsider Al = Al as Al2 -expanding QC-alphabet by ;
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 ;
Al2 = [:NAT,(QC-symbols Al2):] by QC_LANG1:5;
then ( QC-symbols Al2 = (QC-symbols Al1) \/ {s2} & s2 in {s2} ) by ;
then s2 in QC-symbols Al2 by XBOOLE_0:def 3;
then x is bound_QC-variable of Al2 by ;
then consider x2 being bound_QC-variable of Al2 such that
A31: x = x2 ;
All (x2,r2) = All (x,r) by ;
then ( All (x,r) is Element of CQC-WFF Al2 & Al is Al2 -expanding ) ;
hence S1[ All (x,r)] ; :: thesis: verum
end;
then A32: 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, A15, A19;
for p being Element of CQC-WFF Al holds S1[p] from 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