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

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