:: deftheorem Def1 defines finitely_typed LATTICE8:def 1 :
for L being RelStr holds
( L is finitely_typed iff ex A being non empty set st
( ( for e being object st e in the carrier of L holds
e is Equivalence_Relation of A ) & ex o being Element of NAT st
for e1, e2 being Equivalence_Relation of A
for x, y being object st e1 in the carrier of L & e2 in the carrier of L & [x,y] in e1 "\/" e2 holds
ex F being non empty FinSequence of A st
( len F = o & x,y are_joint_by F,e1,e2 ) ) );