defpred S₁[ set ] means ( ( for a being set st a in $1 holds
a is FinSequence of NAT ) & ( for n being Element of NAT holds atom. n in $1 ) & ( for p being FinSequence of NAT st p in $1 holds
'not' p in $1 ) & ( for p, q being FinSequence of NAT st p in $1 & q in $1 holds
p '&' q in $1 ) & ( for p being FinSequence of NAT st p in $1 holds
EX p in $1 ) & ( for p being FinSequence of NAT st p in $1 holds
EG p in $1 ) & ( for p, q being FinSequence of NAT st p in $1 & q in $1 holds
p EU q in $1 ) );
defpred S₂[ object ] means for D being non empty set st S₁[D] holds
$1 in D;
consider Y being set such that
A1: for a being object holds
( a in Y iff ( a in NAT * & S₂[a] ) ) from XBOOLE_0:sch 1();

set a = atom. 0;
A2: for D being non empty set st S₁[D] holds
atom. 0 in D ;
take b = atom. 0; :: thesis:
atom. 0 in NAT * by FINSEQ_1:def 11;
hence b in Y by A1, A2; :: thesis:

end;

then reconsider Y = Y as non empty set ;
take Y ; :: thesis:
thus for a being set st a in Y holds
a is FinSequence of NAT :: thesis:

proof

let a be set ; :: thesis:
assume a in Y ; :: thesis:
then a in NAT * by A1;
hence a is FinSequence of NAT by FINSEQ_1:def 11; :: thesis:

end;

thus for n being Element of NAT holds atom. n in Y :: thesis:

proof

let n be Element of NAT ; :: thesis:
A3: for D being non empty set st S₁[D] holds
atom. n in D ;
atom. n in NAT * by FINSEQ_1:def 11;
hence atom. n in Y by A1, A3; :: thesis:

end;

thus for p being FinSequence of NAT st p in Y holds
'not' p in Y :: thesis:

proof

let p be FinSequence of NAT ; :: thesis:
assume A4: p in Y ; :: thesis:
A5: for D being non empty set st S₁[D] holds
'not' p in D

proof

let D be non empty set ; :: thesis:
assume A6: S₁[D] ; :: thesis:
then p in D by A1, A4;
hence 'not' p in D by A6; :: thesis:

end;

'not' p in NAT * by FINSEQ_1:def 11;
hence 'not' p in Y by A1, A5; :: thesis:

end;

thus for q, p being FinSequence of NAT st q in Y & p in Y holds
q '&' p in Y :: thesis:

proof

let q, p be FinSequence of NAT ; :: thesis:
assume that
A7: q in Y and
A8: p in Y ; :: thesis:
A9: for D being non empty set st S₁[D] holds
q '&' p in D

proof

let D be non empty set ; :: thesis:
assume A10: S₁[D] ; :: thesis:
then A11: q in D by A1, A7;
p in D by A1, A8, A10;
hence q '&' p in D by A10, A11; :: thesis:

end;

q '&' p in NAT * by FINSEQ_1:def 11;
hence q '&' p in Y by A1, A9; :: thesis:

end;

thus for p being FinSequence of NAT st p in Y holds
EX p in Y :: thesis:

proof

let p be FinSequence of NAT ; :: thesis:
assume A12: p in Y ; :: thesis:
A13: for D being non empty set st S₁[D] holds
EX p in D

proof

let D be non empty set ; :: thesis:
assume A14: S₁[D] ; :: thesis:
then p in D by A1, A12;
hence EX p in D by A14; :: thesis:

end;

EX p in NAT * by FINSEQ_1:def 11;
hence EX p in Y by A1, A13; :: thesis:

end;

thus for p being FinSequence of NAT st p in Y holds
EG p in Y :: thesis:

proof

let p be FinSequence of NAT ; :: thesis:
assume A15: p in Y ; :: thesis:
A16: for D being non empty set st S₁[D] holds
EG p in D

proof

let D be non empty set ; :: thesis:
assume A17: S₁[D] ; :: thesis:
then p in D by A1, A15;
hence EG p in D by A17; :: thesis:

end;

EG p in NAT * by FINSEQ_1:def 11;
hence EG p in Y by A1, A16; :: thesis:

end;

thus for q, p being FinSequence of NAT st q in Y & p in Y holds
q EU p in Y :: thesis:

proof

let q, p be FinSequence of NAT ; :: thesis:
assume that
A18: q in Y and
A19: p in Y ; :: thesis:
A20: for D being non empty set st S₁[D] holds
q EU p in D

proof

let D be non empty set ; :: thesis:
assume A21: S₁[D] ; :: thesis:
then A22: q in D by A1, A18;
p in D by A1, A19, A21;
hence q EU p in D by A21, A22; :: thesis:

end;

q EU p in NAT * by FINSEQ_1:def 11;
hence q EU p in Y by A1, A20; :: thesis:

end;

let D be non empty set ; :: thesis:
assume A23: S₁[D] ; :: thesis:
let a be object ; :: according to TARSKI:def 3 :: thesis:
assume a in Y ; :: thesis:
hence a in D by A1, A23; :: thesis: