theorem Th8: :: LATTICE8:8

for A being non trivial set
for L being non empty full finitely_typed Sublattice of EqRelLATT A
for e being Equivalence_Relation of A st e in the carrier of L & e <> id A & type_of L <= 2 holds
L is modular