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:
A4: E0 c= NAT * by A2;
for p being FinSequence st p in E0 holds
<*6*> ^ p in E0

let p be FinSequence; :: thesis:
assume A5: p in E0 ; :: thesis:
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

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

end;

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

end;

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

let n be Element of NAT ; :: thesis:
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:

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

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

let E be set ; :: thesis:
assume A15: E is MC-closed ; :: thesis:
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:

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:

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

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

let E be set ; :: thesis:
assume A22: E is MC-closed ; :: thesis:
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:

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:

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

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

let E be set ; :: thesis:
assume A29: E is MC-closed ; :: thesis:
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:

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:

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:
let E be set ; :: thesis:
assume A32: E is MC-closed ; :: thesis:
let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in E0 ; :: thesis:
hence x in E by A2, A32; :: thesis: