let X1 be non empty set ; :: thesis: for cB1 being filter_base of X1
for cF1 being Filter of X1
for cBa1 being basis of cF1 st cBa1 = cB1 holds
<.cB1.] = cF1
let cB1 be filter_base of X1; :: thesis: for cF1 being Filter of X1
for cBa1 being basis of cF1 st cBa1 = cB1 holds
<.cB1.] = cF1
let cF1 be Filter of X1; :: thesis: for cBa1 being basis of cF1 st cBa1 = cB1 holds
<.cB1.] = cF1
let cBa1 be basis of cF1; :: thesis: ( cBa1 = cB1 implies <.cB1.] = cF1 )
assume A1: cBa1 = cB1 ; :: thesis: <.cB1.] = cF1
cF1 = <.(# cBa1).] by CARDFIL2:21;
hence <.cB1.] = cF1 by A1; :: thesis: verum