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 Element of 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 being FinSequence of NAT st p in D1 holds
EX p in D1 ) & ( for p being FinSequence of NAT st p in D1 holds
EG p in D1 ) & ( for p, q being FinSequence of NAT st p in D1 & q in D1 holds
p EU 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 Element of 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 being FinSequence of NAT st p in D holds
EX p in D ) & ( for p being FinSequence of NAT st p in D holds
EG p in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds
p EU q in D ) holds
D1 c= D ) & ( for a being set st a in D2 holds
a is FinSequence of NAT ) & ( for n being Element of 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 being FinSequence of NAT st p in D2 holds
EX p in D2 ) & ( for p being FinSequence of NAT st p in D2 holds
EG p in D2 ) & ( for p, q being FinSequence of NAT st p in D2 & q in D2 holds
p EU 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 Element of 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 being FinSequence of NAT st p in D holds
EX p in D ) & ( for p being FinSequence of NAT st p in D holds
EG p in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds
p EU q in D ) holds
D2 c= D ) implies D1 = D2 )
assume that
A24: for a being set st a in D1 holds
a is FinSequence of NAT and
A25: for n being Element of NAT holds atom. n in D1 and
A26: for p being FinSequence of NAT st p in D1 holds
'not' p in D1 and
A27: for p, q being FinSequence of NAT st p in D1 & q in D1 holds
p '&' q in D1 and
A28: for p being FinSequence of NAT st p in D1 holds
EX p in D1 and
A29: for p being FinSequence of NAT st p in D1 holds
EG p in D1 and
A30: for p, q being FinSequence of NAT st p in D1 & q in D1 holds
p EU q in D1 and
A31: for D being non empty set st ( for a being set st a in D holds
a is FinSequence of NAT ) & ( for n being Element of 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 being FinSequence of NAT st p in D holds
EX p in D ) & ( for p being FinSequence of NAT st p in D holds
EG p in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds
p EU q in D ) holds
D1 c= D and
A32: for a being set st a in D2 holds
a is FinSequence of NAT and
A33: for n being Element of NAT holds atom. n in D2 and
A34: for p being FinSequence of NAT st p in D2 holds
'not' p in D2 and
A35: for p, q being FinSequence of NAT st p in D2 & q in D2 holds
p '&' q in D2 and
A36: for p being FinSequence of NAT st p in D2 holds
EX p in D2 and
A37: for p being FinSequence of NAT st p in D2 holds
EG p in D2 and
A38: for p, q being FinSequence of NAT st p in D2 & q in D2 holds
p EU q in D2 and
A39: for D being non empty set st ( for a being set st a in D holds
a is FinSequence of NAT ) & ( for n being Element of 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 being FinSequence of NAT st p in D holds
EX p in D ) & ( for p being FinSequence of NAT st p in D holds
EG p in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds
p EU q in D ) holds
D2 c= D ; :: thesis: D1 = D2
A40: D2 c= D1 by A24, A25, A26, A27, A28, A29, A30, A39;
D1 c= D2 by A31, A32, A33, A34, A35, A36, A37, A38;
hence D1 = D2 by A40, XBOOLE_0:def 10; :: thesis: verum