let X be non empty set ; :: thesis: for F being Filter of X
for B1, B2 being basis of F holds # B1, # B2 are_equivalent_generators
let F be Filter of X; :: thesis: for B1, B2 being basis of F holds # B1, # B2 are_equivalent_generators
let B1, B2 be basis of F; :: thesis: # B1, # B2 are_equivalent_generators
hereby :: according to CARDFIL2:def 9 :: thesis: for b2 being Element of # B2 ex b1 being Element of # B1 st b1 c= b2
let b1 be Element of # B1; :: thesis: ex b2 being Element of # B2 st b2 c= b1
b1 in # B1 ;
then b1 in F ;
then b1 in <.(# B2).] by Th06;
hence ex b2 being Element of # B2 st b2 c= b1 by def3; :: thesis: verum
end;
let b2 be Element of # B2; :: thesis: ex b1 being Element of # B1 st b1 c= b2
b2 in # B2 ;
then b2 in F ;
then b2 in <.(# B1).] by Th06;
hence ex b1 being Element of # B1 st b1 c= b2 by def3; :: thesis: verum