:: deftheorem defines has_a_representation_of_type<= LATTICE8:def 2 :
for L being lower-bounded LATTICE
for n being Element of NAT holds
( L has_a_representation_of_type<= n iff ex A being non trivial set ex f being Homomorphism of L,(EqRelLATT A) st
( f is V17() & Image f is finitely_typed & ex e being Equivalence_Relation of A st
( e in the carrier of (Image f) & e <> id A ) & type_of (Image f) <= n ) );