let X be non empty set ; :: thesis: for cF being Filter of X ex cB being filter_base of X st

( cB = cF & <.cB.) = cF )

let cF be Filter of X; :: thesis: ex cB being filter_base of X st

( cB = cF & <.cB.) = cF )

cF is basis of cF by CARDFIL2:13;

then reconsider cB = cF as filter_base of X by CARDFIL2:29;

take cB ; :: thesis: ( cB = cF & <.cB.) = cF )

hence ( cB = cF & <.cB.) = cF ) ; :: thesis: verum

( cB = cF & <.cB.) = cF )

let cF be Filter of X; :: thesis: ex cB being filter_base of X st

( cB = cF & <.cB.) = cF )

cF is basis of cF by CARDFIL2:13;

then reconsider cB = cF as filter_base of X by CARDFIL2:29;

take cB ; :: thesis: ( cB = cF & <.cB.) = cF )

now :: thesis: ( ( for x being object st x in <.cB.) holds

x in cF ) & ( for x being object st x in cF holds

x in <.cB.) ) )

assume x in cF ; :: thesis: x in <.cB.)

hence x in <.cB.) by CARDFIL2:def 8; :: thesis: verum

end;

then
( <.cB.) c= cF & cF c= <.cB.) )
;x in cF ) & ( for x being object st x in cF holds

x in <.cB.) ) )

hereby :: thesis: for x being object st x in cF holds

x in <.cB.)

let x be object ; :: thesis: ( x in cF implies x in <.cB.) )x in <.cB.)

let x be object ; :: thesis: ( x in <.cB.) implies x in cF )

assume A1: x in <.cB.) ; :: thesis: x in cF

then reconsider y = x as Subset of X ;

ex b being Element of cB st b c= y by A1, CARDFIL2:def 8;

hence x in cF by CARD_FIL:def 1; :: thesis: verum

end;assume A1: x in <.cB.) ; :: thesis: x in cF

then reconsider y = x as Subset of X ;

ex b being Element of cB st b c= y by A1, CARDFIL2:def 8;

hence x in cF by CARD_FIL:def 1; :: thesis: verum

assume x in cF ; :: thesis: x in <.cB.)

hence x in <.cB.) by CARDFIL2:def 8; :: thesis: verum

hence ( cB = cF & <.cB.) = cF ) ; :: thesis: verum