for x being Element of [:base_of_frechet_filter,base_of_frechet_filter:] ex i, j being Nat st x = [:(NAT \ (Segm i)),(NAT \ (Segm j)):]