:: deftheorem Def3 defines height LATTICE7:def 3 :
for L being finite LATTICE
for x being Element of L
for b₃ being Element of NAT holds
( b₃ = height x iff ( ex A being Chain of Bottom L,x st b₃ = card A & ( for A being Chain of Bottom L,x holds card A <= b₃ ) ) );