theorem Th21: :: CARDFIL4:22

for n being Nat
for B being Subset of NAT st B = NAT \ (Segm n) holds
B is Element of base_of_frechet_filter