theorem :: FILTER_1:47

for L1, L2 being Lattice holds
( ( L1 is implicative & L2 is implicative ) iff [:L1,L2:] is implicative )