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

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