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