theorem Th4: :: CARDFIL3:5

for I being set holds [#] (OrderedFIN I) is directed