for L being LATTICE st L is modular holds
( L is distributive iff for K being full Sublattice of L holds not M_3 ,K are_isomorphic )