theorem :: BOR_CANT:12

for Omega being non empty set
for Sigma being SigmaField of Omega
for A being SetSequence of Sigma holds
( superior_setsequence A = Union_Shift_Seq A & inferior_setsequence A = Intersect_Shift_Seq A ) by Th11;