theorem Th21: :: CARDFIL2:48

ex F being sequence of (bool NAT) st
for x being Element of NAT holds F . x = { y where y is Element of NAT : x <= y }