theorem Th43: :: SETLIM_1:43

for X being set
for B being SetSequence of X st B is non-descending holds
Intersection (superior_setsequence B) = Union B