for B being B_Lattice
for FB being Filter of B
for I being I_Lattice
for i, j, k being Element of I
for FI being Filter of I
for a, b, c being Element of B holds
( ( i,j are_equivalence_wrt FI & j,k are_equivalence_wrt FI implies i,k are_equivalence_wrt FI ) & ( a,b are_equivalence_wrt FB & b,c are_equivalence_wrt FB implies a,c are_equivalence_wrt FB ) ) by Th62;