let D1, D2 be non empty set ; :: thesis: ( ( for a being set st a in D1 holds
a is FinSequence of NAT ) & ( for x, y being Variable holds
( x '=' y in D1 & x 'in' y 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 x being Variable
for p being FinSequence of NAT st p in D1 holds
All (x,p) in D1 ) & ( for D being non empty set st ( for a being set st a in D holds
a is FinSequence of NAT ) & ( for x, y being Variable holds
( x '=' y in D & x 'in' y 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 x being Variable
for p being FinSequence of NAT st p in D holds
All (x,p) in D ) holds
D1 c= D ) & ( for a being set st a in D2 holds
a is FinSequence of NAT ) & ( for x, y being Variable holds
( x '=' y in D2 & x 'in' y 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 x being Variable
for p being FinSequence of NAT st p in D2 holds
All (x,p) in D2 ) & ( for D being non empty set st ( for a being set st a in D holds
a is FinSequence of NAT ) & ( for x, y being Variable holds
( x '=' y in D & x 'in' y 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 x being Variable
for p being FinSequence of NAT st p in D holds
All (x,p) 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 x, y being Variable holds
( x '=' y in D1 & x 'in' y 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 x being Variable
for p being FinSequence of NAT st p in D1 holds
All (x,p) in D1 ) & ( for D being non empty set st ( for a being set st a in D holds
a is FinSequence of NAT ) & ( for x, y being Variable holds
( x '=' y in D & x 'in' y 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 x being Variable
for p being FinSequence of NAT st p in D holds
All (x,p) in D ) holds
D1 c= D ) & ( for a being set st a in D2 holds
a is FinSequence of NAT ) & ( for x, y being Variable holds
( x '=' y in D2 & x 'in' y 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 x being Variable
for p being FinSequence of NAT st p in D2 holds
All (x,p) in D2 ) & ( for D being non empty set st ( for a being set st a in D holds
a is FinSequence of NAT ) & ( for x, y being Variable holds
( x '=' y in D & x 'in' y 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 x being Variable
for p being FinSequence of NAT st p in D holds
All (x,p) 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