theorem Th17: :: SETLIM_1:17

for X being set
for B being SetSequence of X holds (inferior_setsequence B) . 0 = Intersection B