theorem :: POSET_2:17

for L being non empty finite lower-bounded LATTICE holds
( L is flat iff for x being Element of L holds height x <= 2 )