defpred S₁[ set ] means ( ( for a being set st a in $1 holds
a is FinSequence of NAT ) & ( for n being 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, q being FinSequence of NAT st p in $1 & q in $1 holds
p 'or' q in $1 ) & ( for p being FinSequence of NAT st p in $1 holds
'X' p in $1 ) & ( for p, q being FinSequence of NAT st p in $1 & q in $1 holds
p 'U' q in $1 ) & ( for p, q being FinSequence of NAT st p in $1 & q in $1 holds
p 'R' q in $1 ) );
defpred S₂[ set ] means for D being non empty set st S₁[D] holds
$1 in D;
consider Y being set such that
A1: for a being set holds
( a in Y iff ( a in NAT * & S₂[a] ) ) from XBOOLE_0:sch 1();

now

set a = atom. 0 ;
A2: atom. 0 in NAT * by FINSEQ_1:def 11;
A3: for D being non empty set st S₁[D] holds
atom. 0 in D ;
take b = atom. 0 ; :: thesis:
thus b in Y by A1, A2, A3; :: 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 Nat holds atom. n in Y :: thesis:

proof

let n be Nat; :: thesis:
B1: atom. n in NAT * by FINSEQ_1:def 11;
for D being non empty set st S₁[D] holds
atom. n in D ;
hence atom. n in Y by A1, B1; :: 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 B1: p in Y ; :: thesis:
B2: 'not' p in NAT * by FINSEQ_1:def 11;
for D being non empty set st S₁[D] holds
'not' p in D

proof

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

end;

hence 'not' p in Y by A1, B2; :: 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 B1: ( q in Y & p in Y ) ; :: thesis:
B2: q '&' p in NAT * by FINSEQ_1:def 11;
for D being non empty set st S₁[D] holds
q '&' p in D

proof

let D be non empty set ; :: thesis:
assume B3: S₁[D] ; :: thesis:
then ( p in D & q in D ) by A1, B1;
hence q '&' p in D by B3; :: thesis:

end;

hence q '&' p in Y by A1, B2; :: thesis:

end;

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

proof

let q, p be FinSequence of NAT ; :: thesis:
assume B1: ( q in Y & p in Y ) ; :: thesis:
B2: q 'or' p in NAT * by FINSEQ_1:def 11;
for D being non empty set st S₁[D] holds
q 'or' p in D

proof

let D be non empty set ; :: thesis:
assume B3: S₁[D] ; :: thesis:
then ( p in D & q in D ) by A1, B1;
hence q 'or' p in D by B3; :: thesis:

end;

hence q 'or' p in Y by A1, B2; :: thesis:

end;

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

proof

let p be FinSequence of NAT ; :: thesis:
assume B1: p in Y ; :: thesis:
B2: 'X' p in NAT * by FINSEQ_1:def 11;
for D being non empty set st S₁[D] holds
'X' p in D

proof

let D be non empty set ; :: thesis:
assume B3: S₁[D] ; :: thesis:
then p in D by A1, B1;
hence 'X' p in D by B3; :: thesis:

end;

hence 'X' p in Y by A1, B2; :: thesis:

end;

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

proof

let q, p be FinSequence of NAT ; :: thesis:
assume B1: ( q in Y & p in Y ) ; :: thesis:
B2: q 'U' p in NAT * by FINSEQ_1:def 11;
for D being non empty set st S₁[D] holds
q 'U' p in D

proof

let D be non empty set ; :: thesis:
assume B3: S₁[D] ; :: thesis:
then ( p in D & q in D ) by A1, B1;
hence q 'U' p in D by B3; :: thesis:

end;

hence q 'U' p in Y by A1, B2; :: thesis:

end;

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

proof

let q, p be FinSequence of NAT ; :: thesis:
assume B1: ( q in Y & p in Y ) ; :: thesis:
B2: q 'R' p in NAT * by FINSEQ_1:def 11;
for D being non empty set st S₁[D] holds
q 'R' p in D

proof

let D be non empty set ; :: thesis:
assume B3: S₁[D] ; :: thesis:
then ( p in D & q in D ) by A1, B1;
hence q 'R' p in D by B3; :: thesis:

end;

hence q 'R' p in Y by A1, B2; :: thesis:

end;

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