theorem Th25: :: CARDFIL2:52

for 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 } ) holds
rng F is basis of (Frechet_Filter NAT)