reconsider bff = base_of_frechet_filter as basis of (Frechet_Filter NAT) by CARDFIL2:56;
[:bff,bff:] is basis of <.(Frechet_Filter NAT),(Frechet_Filter NAT).) ;
hence ex cB being basis of (Frechet_Filter NAT) st
( cB = base_of_frechet_filter & [:cB,cB:] is basis of <.(Frechet_Filter NAT),(Frechet_Filter NAT).) ) ; :: thesis: verum