for I being I_Lattice
for FI being Filter of I holds the L_join of I is BinOp of the carrier of I, equivalence_wrt FI