theorem Th18: :: SETLIM_1:18
for X being set
for B being SetSequence of X holds (superior_setsequence B) . 0 = Union B