A1: <*0*> in NAT * by FINSEQ_1:def 11;
defpred S₁[ object ] means for E being set st E is MC-closed holds
$1 in E;
consider E0 being set such that
A2: for x being object holds
( x in E0 iff ( x in NAT * & S₁[x] ) ) from XBOOLE_0:sch 1();
A3: for E being set st E is MC-closed holds
<*0*> in E by Def1;
then reconsider E0 = E0 as non empty set by A2, A1;
take E0 ; :: thesis: ( E0 is MC-closed & ( for E being set st E is MC-closed holds
E0 c= E ) )
A4: E0 c= NAT * by A2;
for p being FinSequence st p in E0 holds
<*6*> ^ p in E0

proof

let p be FinSequence; :: thesis: ( p in E0 implies <*6*> ^ p in E0 )
assume A5: p in E0 ; :: thesis: <*6*> ^ p in E0
p in NAT * by A2, A5;
then reconsider p9 = p as FinSequence of NAT by FINSEQ_1:def 11;
A6: for E being set st E is MC-closed holds
<*6*> ^ p in E

proof

let E be set ; :: thesis: ( E is MC-closed implies <*6*> ^ p in E )
assume A7: E is MC-closed ; :: thesis: <*6*> ^ p in E
then p in E by A2, A5;
hence <*6*> ^ p in E by A7, Def6; :: thesis: verum

end;

<*6*> ^ p9 in NAT * by FINSEQ_1:def 11;
hence <*6*> ^ p in E0 by A2, A6; :: thesis: verum

end;

then A8: E0 is with_modal_operator ;
for n being Element of NAT holds <*(5 + (2 * n))*> in E0

proof

let n be Element of NAT ; :: thesis: <*(5 + (2 * n))*> in E0
set p = 5 + (2 * n);
reconsider h = <*(5 + (2 * n))*> as FinSequence of NAT ;
A9: h in NAT * by FINSEQ_1:def 11;
for E being set st E is MC-closed holds
<*(5 + (2 * n))*> in E by Def5;
hence <*(5 + (2 * n))*> in E0 by A2, A9; :: thesis: verum

end;

then A10: E0 is with_int_propositional_variables ;
for p, q being FinSequence st p in E0 & q in E0 holds
(<*3*> ^ p) ^ q in E0

proof

let p, q be FinSequence; :: thesis: ( p in E0 & q in E0 implies (<*3*> ^ p) ^ q in E0 )
assume that
A11: p in E0 and
A12: q in E0 ; :: thesis: (<*3*> ^ p) ^ q in E0
A13: q in NAT * by A2, A12;
A14: for E being set st E is MC-closed holds
(<*3*> ^ p) ^ q in E

proof

let E be set ; :: thesis: ( E is MC-closed implies (<*3*> ^ p) ^ q in E )
assume A15: E is MC-closed ; :: thesis: (<*3*> ^ p) ^ q in E
then A16: q in E by A2, A12;
p in E by A2, A11, A15;
hence (<*3*> ^ p) ^ q in E by A15, A16, Def4; :: thesis: verum

end;

p in NAT * by A2, A11;
then reconsider p9 = p, q9 = q as FinSequence of NAT by A13, FINSEQ_1:def 11;
(<*3*> ^ p9) ^ q9 in NAT * by FINSEQ_1:def 11;
hence (<*3*> ^ p) ^ q in E0 by A2, A14; :: thesis: verum

end;

then A17: E0 is with_int_disjunction ;
for p, q being FinSequence st p in E0 & q in E0 holds
(<*2*> ^ p) ^ q in E0

proof

let p, q be FinSequence; :: thesis: ( p in E0 & q in E0 implies (<*2*> ^ p) ^ q in E0 )
assume that
A18: p in E0 and
A19: q in E0 ; :: thesis: (<*2*> ^ p) ^ q in E0
A20: q in NAT * by A2, A19;
A21: for E being set st E is MC-closed holds
(<*2*> ^ p) ^ q in E

proof

let E be set ; :: thesis: ( E is MC-closed implies (<*2*> ^ p) ^ q in E )
assume A22: E is MC-closed ; :: thesis: (<*2*> ^ p) ^ q in E
then A23: q in E by A2, A19;
p in E by A2, A18, A22;
hence (<*2*> ^ p) ^ q in E by A22, A23, Def3; :: thesis: verum

end;

p in NAT * by A2, A18;
then reconsider p9 = p, q9 = q as FinSequence of NAT by A20, FINSEQ_1:def 11;
(<*2*> ^ p9) ^ q9 in NAT * by FINSEQ_1:def 11;
hence (<*2*> ^ p) ^ q in E0 by A2, A21; :: thesis: verum

end;

then A24: E0 is with_int_conjunction ;
for p, q being FinSequence st p in E0 & q in E0 holds
(<*1*> ^ p) ^ q in E0

proof

let p, q be FinSequence; :: thesis: ( p in E0 & q in E0 implies (<*1*> ^ p) ^ q in E0 )
assume that
A25: p in E0 and
A26: q in E0 ; :: thesis: (<*1*> ^ p) ^ q in E0
A27: q in NAT * by A2, A26;
A28: for E being set st E is MC-closed holds
(<*1*> ^ p) ^ q in E

proof

let E be set ; :: thesis: ( E is MC-closed implies (<*1*> ^ p) ^ q in E )
assume A29: E is MC-closed ; :: thesis: (<*1*> ^ p) ^ q in E
then A30: q in E by A2, A26;
p in E by A2, A25, A29;
hence (<*1*> ^ p) ^ q in E by A29, A30, Def2; :: thesis: verum

end;

p in NAT * by A2, A25;
then reconsider p9 = p, q9 = q as FinSequence of NAT by A27, FINSEQ_1:def 11;
(<*1*> ^ p9) ^ q9 in NAT * by FINSEQ_1:def 11;
hence (<*1*> ^ p) ^ q in E0 by A2, A28; :: thesis: verum

end;

then A31: E0 is with_int_implication ;
<*0*> in E0 by A2, A1, A3;
then E0 is with_FALSUM ;
hence E0 is MC-closed by A4, A10, A31, A24, A17, A8; :: thesis: for E being set st E is MC-closed holds
E0 c= E
let E be set ; :: thesis: ( E is MC-closed implies E0 c= E )
assume A32: E is MC-closed ; :: thesis: E0 c= E
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in E0 or x in E )
assume x in E0 ; :: thesis: x in E
hence x in E by A2, A32; :: thesis: verum