theorem :: LATTICE7:16

for L being finite LATTICE holds
( L is distributive iff ex X being non empty Ring_of_sets st L, InclPoset X are_isomorphic )