theorem Th5: :: LATTICE8:5
for L1, L2 being lower-bounded LATTICE st L1,L2 are_isomorphic & L1 is modular holds
L2 is modular