let X be non empty set ; :: thesis: for F being Filter of X
for B being basis of F
for S being Subset-Family of X
for S1 being Subset of F st S = S1 & # B,S are_equivalent_generators holds
S1 is basis of F
let F be Filter of X; :: thesis: for B being basis of F
for S being Subset-Family of X
for S1 being Subset of F st S = S1 & # B,S are_equivalent_generators holds
S1 is basis of F
let B be basis of F; :: thesis: for S being Subset-Family of X
for S1 being Subset of F st S = S1 & # B,S are_equivalent_generators holds
S1 is basis of F
let S be Subset-Family of X; :: thesis: for S1 being Subset of F st S = S1 & # B,S are_equivalent_generators holds
S1 is basis of F
let S1 be Subset of F; :: thesis: ( S = S1 & # B,S are_equivalent_generators implies S1 is basis of F )
assume that
A1: S = S1 and
A2: # B,S are_equivalent_generators ; :: thesis: S1 is basis of F
<.(# B).] = <.S.] by A2, Th05;
hence S1 is basis of F by A1, Th06, Th07; :: thesis: verum