0 is QC-symbol of A by Th3;
then <*[0,0]*> is FinSequence of [:NAT,(QC-symbols A):] by Lm2;
then A1: <*[0,0]*> in [:NAT,(QC-symbols A):] * by FINSEQ_1:def 11;
defpred S₁[ object ] means for D being non empty set st D is A -closed holds
$1 in D;
consider D0 being set such that
A2: for x being object holds
( x in D0 iff ( x in [:NAT,(QC-symbols A):] * & S₁[x] ) ) from XBOOLE_0:sch 1();
A3: for D being non empty set st D is A -closed holds
<*[0,0]*> in D ;
then reconsider D0 = D0 as non empty set by A2, A1;
take D0 ; :: thesis: ( D0 is A -closed & ( for D being non empty set st D is A -closed holds
D0 c= D ) )
D0 c= [:NAT,(QC-symbols A):] * by A2;
hence D0 is Subset of ([:NAT,(QC-symbols A):] *) ; :: according to QC_LANG1:def 10 :: thesis: ( ( for k being Nat
for p being QC-pred_symbol of k,A
for ll being QC-variable_list of k,A holds <*p*> ^ ll in D0 ) & <*[0,0]*> in D0 & ( for p being FinSequence of [:NAT,(QC-symbols A):] st p in D0 holds
<*[1,0]*> ^ p in D0 ) & ( for p, q being FinSequence of [:NAT,(QC-symbols A):] st p in D0 & q in D0 holds
(<*[2,0]*> ^ p) ^ q in D0 ) & ( for x being bound_QC-variable of A
for p being FinSequence of [:NAT,(QC-symbols A):] st p in D0 holds
(<*[3,0]*> ^ <*x*>) ^ p in D0 ) & ( for D being non empty set st D is A -closed holds
D0 c= D ) )
thus for k being Nat
for p being QC-pred_symbol of k,A
for ll being QC-variable_list of k,A holds <*p*> ^ ll in D0 :: thesis: ( <*[0,0]*> in D0 & ( for p being FinSequence of [:NAT,(QC-symbols A):] st p in D0 holds
<*[1,0]*> ^ p in D0 ) & ( for p, q being FinSequence of [:NAT,(QC-symbols A):] st p in D0 & q in D0 holds
(<*[2,0]*> ^ p) ^ q in D0 ) & ( for x being bound_QC-variable of A
for p being FinSequence of [:NAT,(QC-symbols A):] st p in D0 holds
(<*[3,0]*> ^ <*x*>) ^ p in D0 ) & ( for D being non empty set st D is A -closed holds
D0 c= D ) )

proof

let k be Nat; :: thesis: for p being QC-pred_symbol of k,A
for ll being QC-variable_list of k,A holds <*p*> ^ ll in D0
let p be QC-pred_symbol of k,A; :: thesis: for ll being QC-variable_list of k,A holds <*p*> ^ ll in D0
let ll be QC-variable_list of k,A; :: thesis: <*p*> ^ ll in D0
<*p*> ^ ll is FinSequence of [:NAT,(QC-symbols A):] by Lm3;
then A4: <*p*> ^ ll in [:NAT,(QC-symbols A):] * by FINSEQ_1:def 11;
for D being non empty set st D is A -closed holds
<*p*> ^ ll in D ;
hence <*p*> ^ ll in D0 by A2, A4; :: thesis: verum

end;

thus <*[0,0]*> in D0 by A2, A1, A3; :: thesis: ( ( for p being FinSequence of [:NAT,(QC-symbols A):] st p in D0 holds
<*[1,0]*> ^ p in D0 ) & ( for p, q being FinSequence of [:NAT,(QC-symbols A):] st p in D0 & q in D0 holds
(<*[2,0]*> ^ p) ^ q in D0 ) & ( for x being bound_QC-variable of A
for p being FinSequence of [:NAT,(QC-symbols A):] st p in D0 holds
(<*[3,0]*> ^ <*x*>) ^ p in D0 ) & ( for D being non empty set st D is A -closed holds
D0 c= D ) )
thus for p being FinSequence of [:NAT,(QC-symbols A):] st p in D0 holds
<*[1,0]*> ^ p in D0 :: thesis: ( ( for p, q being FinSequence of [:NAT,(QC-symbols A):] st p in D0 & q in D0 holds
(<*[2,0]*> ^ p) ^ q in D0 ) & ( for x being bound_QC-variable of A
for p being FinSequence of [:NAT,(QC-symbols A):] st p in D0 holds
(<*[3,0]*> ^ <*x*>) ^ p in D0 ) & ( for D being non empty set st D is A -closed holds
D0 c= D ) )

proof

A5: 0 is QC-symbol of A by Th3;
reconsider h = <*[1,0]*> as FinSequence of [:NAT,(QC-symbols A):] by Lm2, A5;
let p be FinSequence of [:NAT,(QC-symbols A):]; :: thesis: ( p in D0 implies <*[1,0]*> ^ p in D0 )
assume A6: p in D0 ; :: thesis: <*[1,0]*> ^ p in D0
A7: for D being non empty set st D is A -closed holds
<*[1,0]*> ^ p in D

proof

let D be non empty set ; :: thesis: ( D is A -closed implies <*[1,0]*> ^ p in D )
assume A8: D is A -closed ; :: thesis: <*[1,0]*> ^ p in D
then p in D by A2, A6;
hence <*[1,0]*> ^ p in D by A8; :: thesis: verum

end;

h ^ p is FinSequence of [:NAT,(QC-symbols A):] ;
then <*[1,0]*> ^ p in [:NAT,(QC-symbols A):] * by FINSEQ_1:def 11;
hence <*[1,0]*> ^ p in D0 by A2, A7; :: thesis: verum

end;

thus for p, q being FinSequence of [:NAT,(QC-symbols A):] st p in D0 & q in D0 holds
(<*[2,0]*> ^ p) ^ q in D0 :: thesis: ( ( for x being bound_QC-variable of A
for p being FinSequence of [:NAT,(QC-symbols A):] st p in D0 holds
(<*[3,0]*> ^ <*x*>) ^ p in D0 ) & ( for D being non empty set st D is A -closed holds
D0 c= D ) )

proof

A9: 0 is QC-symbol of A by Th3;
reconsider h = <*[2,0]*> as FinSequence of [:NAT,(QC-symbols A):] by A9, Lm2;
let p, q be FinSequence of [:NAT,(QC-symbols A):]; :: thesis: ( p in D0 & q in D0 implies (<*[2,0]*> ^ p) ^ q in D0 )
assume A10: ( p in D0 & q in D0 ) ; :: thesis: (<*[2,0]*> ^ p) ^ q in D0
A11: for D being non empty set st D is A -closed holds
(<*[2,0]*> ^ p) ^ q in D

proof

let D be non empty set ; :: thesis: ( D is A -closed implies (<*[2,0]*> ^ p) ^ q in D )
assume A12: D is A -closed ; :: thesis: (<*[2,0]*> ^ p) ^ q in D
then ( p in D & q in D ) by A2, A10;
hence (<*[2,0]*> ^ p) ^ q in D by A12; :: thesis: verum

end;

(h ^ p) ^ q is FinSequence of [:NAT,(QC-symbols A):] ;
then (<*[2,0]*> ^ p) ^ q in [:NAT,(QC-symbols A):] * by FINSEQ_1:def 11;
hence (<*[2,0]*> ^ p) ^ q in D0 by A2, A11; :: thesis: verum

end;

thus for x being bound_QC-variable of A
for p being FinSequence of [:NAT,(QC-symbols A):] st p in D0 holds
(<*[3,0]*> ^ <*x*>) ^ p in D0 :: thesis: for D being non empty set st D is A -closed holds
D0 c= D

proof

let x be bound_QC-variable of A; :: thesis: for p being FinSequence of [:NAT,(QC-symbols A):] st p in D0 holds
(<*[3,0]*> ^ <*x*>) ^ p in D0
let p be FinSequence of [:NAT,(QC-symbols A):]; :: thesis: ( p in D0 implies (<*[3,0]*> ^ <*x*>) ^ p in D0 )
assume A13: p in D0 ; :: thesis: (<*[3,0]*> ^ <*x*>) ^ p in D0
A14: for D being non empty set st D is A -closed holds
(<*[3,0]*> ^ <*x*>) ^ p in D

proof

let D be non empty set ; :: thesis: ( D is A -closed implies (<*[3,0]*> ^ <*x*>) ^ p in D )
assume A15: D is A -closed ; :: thesis: (<*[3,0]*> ^ <*x*>) ^ p in D
then p in D by A2, A13;
hence (<*[3,0]*> ^ <*x*>) ^ p in D by A15; :: thesis: verum

end;

(<*[3,0]*> ^ <*x*>) ^ p is FinSequence of [:NAT,(QC-symbols A):] by Lm4;
then (<*[3,0]*> ^ <*x*>) ^ p in [:NAT,(QC-symbols A):] * by FINSEQ_1:def 11;
hence (<*[3,0]*> ^ <*x*>) ^ p in D0 by A2, A14; :: thesis: verum

end;

let D be non empty set ; :: thesis: ( D is A -closed implies D0 c= D )
assume A16: D is A -closed ; :: thesis: D0 c= D
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in D0 or x in D )
assume x in D0 ; :: thesis: x in D
hence x in D by A2, A16; :: thesis: verum