theorem Th14: :: FILTER_1:14

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