defpred S₁[ set ] means ( ( for a being set st a in $1 holds
a is FinSequence of NAT ) & ( for x, y being Variable holds
( x '=' y in $1 & x 'in' y 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 x being Variable
for p being FinSequence of NAT st p in $1 holds
All (x,p) 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 XFAMILY:sch 1();

set a = (x. 0) '=' (x. 0);
take b = (x. 0) '=' (x. 0); :: thesis:
( (x. 0) '=' (x. 0) in NAT * & ( for D being non empty set st S₁[D] holds
(x. 0) '=' (x. 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:

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 x, y being Variable holds
( x '=' y in Y & x 'in' y in Y ) :: thesis:

let x, y be Variable; :: thesis:
( x '=' y in NAT * & ( for D being non empty set st S₁[D] holds
x '=' y in D ) ) by FINSEQ_1:def 11;
hence x '=' y in Y by A1; :: thesis:
( x 'in' y in NAT * & ( for D being non empty set st S₁[D] holds
x 'in' y in D ) ) by FINSEQ_1:def 11;
hence x 'in' y in Y by A1; :: thesis:

end;

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

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

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:

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

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 x being Variable
for p being FinSequence of NAT st p in Y holds
All (x,p) in Y :: thesis:

let x be Variable; :: thesis:
let p be FinSequence of NAT ; :: thesis:
assume A8: p in Y ; :: thesis:
A9: for D being non empty set st S₁[D] holds
All (x,p) in D

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

end;

All (x,p) in NAT * by FINSEQ_1:def 11;
hence All (x,p) in Y by A1, A9; :: thesis:

end;

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