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 )
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.) ) )
hereby :: thesis: for x being object st x in cF holds
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;
let x be object ; :: thesis: ( x in cF implies 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.) ) ;
hence ( cB = cF & <.cB.) = cF ) ; :: thesis: verum