defpred S1[ 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 S2[ object ] means for D being non empty set st S1[D] holds
$1 in D;
consider Y being set such that
A1:
for a being object holds
( a in Y iff ( a in NAT * & S2[a] ) )
from XBOOLE_0:sch 1();
then reconsider Y = Y as non empty set ;
take
Y
; ( ( for a being set st a in Y holds
a is FinSequence of NAT ) & ( for n being Nat holds atom. n in Y ) & ( for p being FinSequence of NAT st p in Y holds
'not' p in Y ) & ( for p, q being FinSequence of NAT st p in Y & q in Y holds
p '&' q in Y ) & ( for p, q being FinSequence of NAT st p in Y & q in Y holds
p 'or' q in Y ) & ( for p being FinSequence of NAT st p in Y holds
'X' p in Y ) & ( for p, q being FinSequence of NAT st p in Y & q in Y holds
p 'U' q in Y ) & ( for p, q being FinSequence of NAT st p in Y & q in Y holds
p 'R' q in Y ) & ( for D being non empty set st ( for a being set st a in D holds
a is FinSequence of NAT ) & ( for n being Nat holds atom. n in D ) & ( for p being FinSequence of NAT st p in D holds
'not' p in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds
p '&' q in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds
p 'or' q in D ) & ( for p being FinSequence of NAT st p in D holds
'X' p in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds
p 'U' q in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds
p 'R' q in D ) holds
Y c= D ) )
thus
for a being set st a in Y holds
a is FinSequence of NAT
( ( for n being Nat holds atom. n in Y ) & ( for p being FinSequence of NAT st p in Y holds
'not' p in Y ) & ( for p, q being FinSequence of NAT st p in Y & q in Y holds
p '&' q in Y ) & ( for p, q being FinSequence of NAT st p in Y & q in Y holds
p 'or' q in Y ) & ( for p being FinSequence of NAT st p in Y holds
'X' p in Y ) & ( for p, q being FinSequence of NAT st p in Y & q in Y holds
p 'U' q in Y ) & ( for p, q being FinSequence of NAT st p in Y & q in Y holds
p 'R' q in Y ) & ( for D being non empty set st ( for a being set st a in D holds
a is FinSequence of NAT ) & ( for n being Nat holds atom. n in D ) & ( for p being FinSequence of NAT st p in D holds
'not' p in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds
p '&' q in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds
p 'or' q in D ) & ( for p being FinSequence of NAT st p in D holds
'X' p in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds
p 'U' q in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds
p 'R' q in D ) holds
Y c= D ) )
thus
for n being Nat holds atom. n in Y
( ( for p being FinSequence of NAT st p in Y holds
'not' p in Y ) & ( for p, q being FinSequence of NAT st p in Y & q in Y holds
p '&' q in Y ) & ( for p, q being FinSequence of NAT st p in Y & q in Y holds
p 'or' q in Y ) & ( for p being FinSequence of NAT st p in Y holds
'X' p in Y ) & ( for p, q being FinSequence of NAT st p in Y & q in Y holds
p 'U' q in Y ) & ( for p, q being FinSequence of NAT st p in Y & q in Y holds
p 'R' q in Y ) & ( for D being non empty set st ( for a being set st a in D holds
a is FinSequence of NAT ) & ( for n being Nat holds atom. n in D ) & ( for p being FinSequence of NAT st p in D holds
'not' p in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds
p '&' q in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds
p 'or' q in D ) & ( for p being FinSequence of NAT st p in D holds
'X' p in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds
p 'U' q in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds
p 'R' q in D ) holds
Y c= D ) )
thus
for p being FinSequence of NAT st p in Y holds
'not' p in Y
( ( for p, q being FinSequence of NAT st p in Y & q in Y holds
p '&' q in Y ) & ( for p, q being FinSequence of NAT st p in Y & q in Y holds
p 'or' q in Y ) & ( for p being FinSequence of NAT st p in Y holds
'X' p in Y ) & ( for p, q being FinSequence of NAT st p in Y & q in Y holds
p 'U' q in Y ) & ( for p, q being FinSequence of NAT st p in Y & q in Y holds
p 'R' q in Y ) & ( for D being non empty set st ( for a being set st a in D holds
a is FinSequence of NAT ) & ( for n being Nat holds atom. n in D ) & ( for p being FinSequence of NAT st p in D holds
'not' p in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds
p '&' q in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds
p 'or' q in D ) & ( for p being FinSequence of NAT st p in D holds
'X' p in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds
p 'U' q in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds
p 'R' q in D ) holds
Y c= D ) )
thus
for q, p being FinSequence of NAT st q in Y & p in Y holds
q '&' p in Y
( ( for p, q being FinSequence of NAT st p in Y & q in Y holds
p 'or' q in Y ) & ( for p being FinSequence of NAT st p in Y holds
'X' p in Y ) & ( for p, q being FinSequence of NAT st p in Y & q in Y holds
p 'U' q in Y ) & ( for p, q being FinSequence of NAT st p in Y & q in Y holds
p 'R' q in Y ) & ( for D being non empty set st ( for a being set st a in D holds
a is FinSequence of NAT ) & ( for n being Nat holds atom. n in D ) & ( for p being FinSequence of NAT st p in D holds
'not' p in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds
p '&' q in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds
p 'or' q in D ) & ( for p being FinSequence of NAT st p in D holds
'X' p in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds
p 'U' q in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds
p 'R' q in D ) holds
Y c= D ) )
thus
for q, p being FinSequence of NAT st q in Y & p in Y holds
q 'or' p in Y
( ( for p being FinSequence of NAT st p in Y holds
'X' p in Y ) & ( for p, q being FinSequence of NAT st p in Y & q in Y holds
p 'U' q in Y ) & ( for p, q being FinSequence of NAT st p in Y & q in Y holds
p 'R' q in Y ) & ( for D being non empty set st ( for a being set st a in D holds
a is FinSequence of NAT ) & ( for n being Nat holds atom. n in D ) & ( for p being FinSequence of NAT st p in D holds
'not' p in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds
p '&' q in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds
p 'or' q in D ) & ( for p being FinSequence of NAT st p in D holds
'X' p in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds
p 'U' q in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds
p 'R' q in D ) holds
Y c= D ) )
thus
for p being FinSequence of NAT st p in Y holds
'X' p in Y
( ( for p, q being FinSequence of NAT st p in Y & q in Y holds
p 'U' q in Y ) & ( for p, q being FinSequence of NAT st p in Y & q in Y holds
p 'R' q in Y ) & ( for D being non empty set st ( for a being set st a in D holds
a is FinSequence of NAT ) & ( for n being Nat holds atom. n in D ) & ( for p being FinSequence of NAT st p in D holds
'not' p in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds
p '&' q in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds
p 'or' q in D ) & ( for p being FinSequence of NAT st p in D holds
'X' p in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds
p 'U' q in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds
p 'R' q in D ) holds
Y c= D ) )
thus
for q, p being FinSequence of NAT st q in Y & p in Y holds
q 'U' p in Y
( ( for p, q being FinSequence of NAT st p in Y & q in Y holds
p 'R' q in Y ) & ( for D being non empty set st ( for a being set st a in D holds
a is FinSequence of NAT ) & ( for n being Nat holds atom. n in D ) & ( for p being FinSequence of NAT st p in D holds
'not' p in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds
p '&' q in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds
p 'or' q in D ) & ( for p being FinSequence of NAT st p in D holds
'X' p in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds
p 'U' q in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds
p 'R' q in D ) holds
Y c= D ) )
thus
for q, p being FinSequence of NAT st q in Y & p in Y holds
q 'R' p in Y
for D being non empty set st ( for a being set st a in D holds
a is FinSequence of NAT ) & ( for n being Nat holds atom. n in D ) & ( for p being FinSequence of NAT st p in D holds
'not' p in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds
p '&' q in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds
p 'or' q in D ) & ( for p being FinSequence of NAT st p in D holds
'X' p in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds
p 'U' q in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds
p 'R' q in D ) holds
Y c= D
let D be non empty set ; ( ( for a being set st a in D holds
a is FinSequence of NAT ) & ( for n being Nat holds atom. n in D ) & ( for p being FinSequence of NAT st p in D holds
'not' p in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds
p '&' q in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds
p 'or' q in D ) & ( for p being FinSequence of NAT st p in D holds
'X' p in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds
p 'U' q in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds
p 'R' q in D ) implies Y c= D )
assume A20:
S1[D]
; Y c= D
let a be object ; TARSKI:def 3 ( not a in Y or a in D )
assume
a in Y
; a in D
hence
a in D
by A1, A20; verum