theorem Th13: :: LATTICE5:13

for X being non empty set
for Y being Sublattice of EqRelLATT X
for n being Element of NAT st ex e being Equivalence_Relation of X st
( e in the carrier of Y & e <> id X ) & ( for e1, e2 being Equivalence_Relation of X
for x, y being object st e1 in the carrier of Y & e2 in the carrier of Y & [x,y] in e1 "\/" e2 holds
ex F being non empty FinSequence of X st
( len F = n + 2 & x,y are_joint_by F,e1,e2 ) ) holds
type_of Y <= n