theorem :: LATTICE8:36

for L being lower-bounded LATTICE holds
( L has_a_representation_of_type<= 2 iff L is modular ) by Th9, Th35;