let X be non empty set ; :: thesis: for B1, B2 being filter_base of X st <.B1.) = <.B2.) holds
B1,B2 are_equivalent_generators
let B1, B2 be filter_base of X; :: thesis: ( <.B1.) = <.B2.) implies B1,B2 are_equivalent_generators )
assume A1: <.B1.) = <.B2.) ; :: thesis: B1,B2 are_equivalent_generators
A2: for b1 being Element of B1 ex b2 being Element of B2 st b2 c= b1

proof

let b1 be Element of B1; :: thesis: ex b2 being Element of B2 st b2 c= b1
b1 in <.B2.] by A1, def3;
then consider b2 being Element of B2 such that
A3: b2 c= b1 by def3;
thus ex b2 being Element of B2 st b2 c= b1 by A3; :: thesis: verum

end;

for b2 being Element of B2 ex b1 being Element of B1 st b1 c= b2

proof

let b2 be Element of B2; :: thesis: ex b1 being Element of B1 st b1 c= b2
b2 in <.B1.] by A1, def3;
then consider b1 being Element of B1 such that
A4: b1 c= b2 by def3;
thus ex b1 being Element of B1 st b1 c= b2 by A4; :: thesis: verum

end;

hence B1,B2 are_equivalent_generators by A2; :: thesis: verum