theorem Th9: :: LATTICE8:9

for L being lower-bounded LATTICE st L has_a_representation_of_type<= 2 holds
L is modular