theorem :: FILTER_1:37

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