consider F being sequence of (bool NAT) such that
A1: for x being Element of NAT holds F . x = { y where y is Element of NAT : x <= y } by Th21;
set F1 = rng F;
set F2 = { (uparrow p) where p is Element of OrderedNAT : verum } ;
A2: rng F = { (uparrow p) where p is Element of OrderedNAT : verum } by A1, Th26;
hence # (Tails OrderedNAT) is basis of (Frechet_Filter NAT) by A1, Th25; :: thesis: Tails_Filter OrderedNAT = Frechet_Filter NAT
reconsider BFF = # (Tails OrderedNAT) as basis of (Frechet_Filter NAT) by A1, A2, Th25;
<.(# BFF).] = Frechet_Filter NAT by Th06;
hence Tails_Filter OrderedNAT = Frechet_Filter NAT by DefL9; :: thesis: verum