let X be non empty set ; :: thesis: for F being Filter of X
for B being basis of F holds F = <.(# B).]
let F be Filter of X; :: thesis: for B being basis of F holds F = <.(# B).]
let B be basis of F; :: thesis: F = <.(# B).]
hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: <.(# B).] c= F
let x be object ; :: thesis: ( x in F implies x in <.(# B).] )
assume x in F ; :: thesis: x in <.(# B).]
then reconsider x0 = x as Element of F ;
consider b0 being Element of B such that
A1: b0 c= x0 by def2;
reconsider x0 = x0 as Subset of X ;
thus x in <.(# B).] by A1, def3; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in <.(# B).] or x in F )
assume A2: x in <.(# B).] ; :: thesis: x in F
then reconsider x0 = x as Subset of X ;
reconsider B2 = # B as Subset-Family of X ;
consider b0 being Element of B such that
A3: b0 c= x0 by A2, def3;
thus x in F by A3, CARD_FIL:def 1; :: thesis: verum