theorem :: YELLOW11:11
for L being LATTICE holds
( L is modular iff for K being full Sublattice of L holds not N_5 ,K are_isomorphic )