let D1, D2 be non empty set ; :: thesis: ( ( for a being set st a in D1 holds
a is FinSequence of NAT ) & ( for n being Nat holds atom. n in D1 ) & ( for p being FinSequence of NAT st p in D1 holds
'not' p in D1 ) & ( for p, q being FinSequence of NAT st p in D1 & q in D1 holds
p '&' q in D1 ) & ( for p, q being FinSequence of NAT st p in D1 & q in D1 holds
p 'or' q in D1 ) & ( for p being FinSequence of NAT st p in D1 holds
'X' p in D1 ) & ( for p, q being FinSequence of NAT st p in D1 & q in D1 holds
p 'U' q in D1 ) & ( for p, q being FinSequence of NAT st p in D1 & q in D1 holds
p 'R' q in D1 ) & ( 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
D1 c= D ) & ( for a being set st a in D2 holds
a is FinSequence of NAT ) & ( for n being Nat holds atom. n in D2 ) & ( for p being FinSequence of NAT st p in D2 holds
'not' p in D2 ) & ( for p, q being FinSequence of NAT st p in D2 & q in D2 holds
p '&' q in D2 ) & ( for p, q being FinSequence of NAT st p in D2 & q in D2 holds
p 'or' q in D2 ) & ( for p being FinSequence of NAT st p in D2 holds
'X' p in D2 ) & ( for p, q being FinSequence of NAT st p in D2 & q in D2 holds
p 'U' q in D2 ) & ( for p, q being FinSequence of NAT st p in D2 & q in D2 holds
p 'R' q in D2 ) & ( 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
D2 c= D ) implies D1 = D2 )
assume ( ( for a being set st a in D1 holds
a is FinSequence of NAT ) & ( for n being Nat holds atom. n in D1 ) & ( for p being FinSequence of NAT st p in D1 holds
'not' p in D1 ) & ( for p, q being FinSequence of NAT st p in D1 & q in D1 holds
p '&' q in D1 ) & ( for p, q being FinSequence of NAT st p in D1 & q in D1 holds
p 'or' q in D1 ) & ( for p being FinSequence of NAT st p in D1 holds
'X' p in D1 ) & ( for p, q being FinSequence of NAT st p in D1 & q in D1 holds
p 'U' q in D1 ) & ( for p, q being FinSequence of NAT st p in D1 & q in D1 holds
p 'R' q in D1 ) & ( 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
D1 c= D ) & ( for a being set st a in D2 holds
a is FinSequence of NAT ) & ( for n being Nat holds atom. n in D2 ) & ( for p being FinSequence of NAT st p in D2 holds
'not' p in D2 ) & ( for p, q being FinSequence of NAT st p in D2 & q in D2 holds
p '&' q in D2 ) & ( for p, q being FinSequence of NAT st p in D2 & q in D2 holds
p 'or' q in D2 ) & ( for p being FinSequence of NAT st p in D2 holds
'X' p in D2 ) & ( for p, q being FinSequence of NAT st p in D2 & q in D2 holds
p 'U' q in D2 ) & ( for p, q being FinSequence of NAT st p in D2 & q in D2 holds
p 'R' q in D2 ) & ( 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
D2 c= D ) ) ; :: thesis: D1 = D2
then ( D1 c= D2 & D2 c= D1 ) ;
hence D1 = D2 by XBOOLE_0:def 10; :: thesis: verum