theorem Th14: :: BOR_CANT:14

for Omega being non empty set
for Sigma being SigmaField of Omega holds
( ( for X being set
for A being SetSequence of X
for n being Nat
for x being object holds
( ex k being Nat st x in (A ^\ n) . k iff ex k being Nat st
( k >= n & x in A . k ) ) ) & ( for X being set
for A being SetSequence of X
for x being object holds
( x in Intersection (superior_setsequence A) iff for m being Nat ex n being Nat st
( n >= m & x in A . n ) ) ) & ( for A being SetSequence of Sigma
for x being object holds
( x in @Intersection (superior_setsequence A) iff for m being Nat ex n being Nat st
( n >= m & x in A . n ) ) ) & ( for X being set
for A being SetSequence of X
for x being object holds
( x in Union (inferior_setsequence A) iff ex n being Nat st
for k being Nat st k >= n holds
x in A . k ) ) & ( for A being SetSequence of Sigma
for x being object holds
( x in Union (inferior_setsequence A) iff ex n being Nat st
for k being Nat st k >= n holds
x in A . k ) ) & ( for A being SetSequence of Sigma
for x being Element of Omega holds
( x in Union (inferior_setsequence (Complement A)) iff ex n being Nat st
for k being Nat st k >= n holds
not x in A . k ) ) )