theorem Th20: :: CARDFIL4:21

for B being Element of base_of_frechet_filter ex n being Nat st B = NAT \ (Segm n)