theorem Th27: :: CARDFIL2:54

( # (Tails OrderedNAT) is basis of (Frechet_Filter NAT) & Tails_Filter OrderedNAT = Frechet_Filter NAT )