let X1 be non empty set ; :: thesis: for cF1 being Filter of X1 ex cB1 being filter_base of X1 st <.cB1.) = cF1
let cF1 be Filter of X1; :: thesis: ex cB1 being filter_base of X1 st <.cB1.) = cF1
A1: cF1 is basis of cF1 by CARDFIL2:13;
then reconsider cB1 = cF1 as filter_base of X1 by CARDFIL2:29;
<.cB1.) = <.cB1.] ;
hence ex cB1 being filter_base of X1 st <.cB1.) = cF1 by A1, Th23; :: thesis: verum