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₁[ 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₁[ VERUM Al]

proof

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₁[ 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 S₁[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 S₁[P ! l]
let P be QC-pred_symbol of k,Al; :: thesis: for l being CQC-variable_list of k,Al holds S₁[P ! l]
let l be CQC-variable_list of k,Al; :: thesis: S₁[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

proof

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;

then A14: rng l c= 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₁[P ! l] ; :: thesis: verum

end;

A15: for r being Element of CQC-WFF Al st S₁[r] holds
S₁[ 'not' r]

proof

let r be Element of CQC-WFF Al; :: thesis: ( S₁[r] implies S₁[ 'not' r] )
assume A16: S₁[r] ; :: thesis: S₁[ '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₁[ 'not' r] by A17; :: thesis: verum

end;

A19: for r, s being Element of CQC-WFF Al st S₁[r] & S₁[s] holds
S₁[r '&' s]

proof

let r, s be Element of CQC-WFF Al; :: thesis: ( S₁[r] & S₁[s] implies S₁[r '&' s] )
assume A20: ( S₁[r] & S₁[s] ) ; :: thesis: S₁[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₁[r '&' s] ; :: thesis: verum

end;

for x being bound_QC-variable of Al
for r being Element of CQC-WFF Al st S₁[r] holds
S₁[ All (x,r)]

proof

let x be bound_QC-variable of Al; :: thesis: for r being Element of CQC-WFF Al st S₁[r] holds
S₁[ All (x,r)]
let r be Element of CQC-WFF Al; :: thesis: ( S₁[r] implies S₁[ All (x,r)] )
assume A24: S₁[r] ; :: thesis: S₁[ 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₁[ 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
( S₁[ VERUM Al] & S₁[P ! l] & ( S₁[r] implies S₁[ 'not' r] ) & ( S₁[r] & S₁[s] implies S₁[r '&' s] ) & ( S₁[r] implies S₁[ All (x,r)] ) ) by A1, A2, A15, A19;
for p being Element of CQC-WFF Al holds S₁[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