for A being non empty set
for L being non empty Sublattice of EqRelLATT A holds
( L is trivial or ex e being Equivalence_Relation of A st
( e in the carrier of L & e <> id A ) )