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

let b1 be Element of B1; :: thesis:
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:

end;

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

let b2 be Element of B2; :: thesis:
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:

end;