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₂[ 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;
take b = atom. 0; :: thesis:
( atom. 0 in NAT * & ( for D being non empty set st S₁[D] holds
atom. 0 in D ) ) by FINSEQ_1:def 11;
hence b in Y by A1; :: 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:
( atom. n in NAT * & ( for D being non empty set st S₁[D] holds
atom. n in D ) ) by FINSEQ_1:def 11;
hence atom. n in Y by A1; :: 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 A2: p in Y ; :: thesis:
A3: for D being non empty set st S₁[D] holds
'not' p in D

proof

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

end;

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

proof

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

end;

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

proof

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

end;

q 'or' p in NAT * by FINSEQ_1:def 11;
hence q 'or' p in Y by A1, A9; :: 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 A11: p in Y ; :: thesis:
A12: for D being non empty set st S₁[D] holds
'X' p in D

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

end;

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