theorem Th18: :: SETLIM_1:18

for X being set
for B being SetSequence of X holds (superior_setsequence B) . 0 = Union B