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 S1[ 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):] * & S1[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
; ( 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):] *)
; QC_LANG1:def 10 ( ( 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
( <*[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
<*[0,0]*> in D0
by A2, A1, A3; ( ( 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
( ( 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):];
( p in D0 implies <*[1,0]*> ^ p in D0 )
assume A6:
p in D0
;
<*[1,0]*> ^ p in D0
A7:
for
D being non
empty set st
D is
A -closed holds
<*[1,0]*> ^ p in D
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;
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
( ( 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):];
( p in D0 & q in D0 implies (<*[2,0]*> ^ p) ^ q in D0 )
assume A10:
(
p in D0 &
q in D0 )
;
(<*[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
(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;
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
for D being non empty set st D is A -closed holds
D0 c= Dproof
let x be
bound_QC-variable of
A;
for p being FinSequence of [:NAT,(QC-symbols A):] st p in D0 holds
(<*[3,0]*> ^ <*x*>) ^ p in D0let p be
FinSequence of
[:NAT,(QC-symbols A):];
( p in D0 implies (<*[3,0]*> ^ <*x*>) ^ p in D0 )
assume A13:
p in D0
;
(<*[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
(<*[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;
verum
end;
let D be non empty set ; ( D is A -closed implies D0 c= D )
assume A16:
D is A -closed
; D0 c= D
let x be object ; TARSKI:def 3 ( not x in D0 or x in D )
assume
x in D0
; x in D
hence
x in D
by A2, A16; verum