theorem Th31: :: CARDFIL4:38

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)):]