let L be LATTICE; :: thesis: ( L is modular implies ( L is distributive iff for K being full Sublattice of L holds not M_3 ,K are_isomorphic ) )
assume A1: L is modular ; :: thesis: ( L is distributive iff for K being full Sublattice of L holds not M_3 ,K are_isomorphic )
thus ( L is distributive implies for K being full Sublattice of L holds not M_3 ,K are_isomorphic ) :: thesis: ( ( for K being full Sublattice of L holds not M_3 ,K are_isomorphic ) implies L is distributive )

proof

assume L is distributive ; :: thesis: for K being full Sublattice of L holds not M_3 ,K are_isomorphic
then for a, b, c, d, e being Element of L holds
( not a <> b or not a <> c or not a <> d or not a <> e or not b <> c or not b <> d or not b <> e or not c <> d or not c <> e or not d <> e or not a "/\" b = a or not a "/\" c = a or not a "/\" d = a or not b "/\" e = b or not c "/\" e = c or not d "/\" e = d or not b "/\" c = a or not b "/\" d = a or not c "/\" d = a or not b "\/" c = e or not b "\/" d = e or not c "\/" d = e ) by Lm3;
hence for K being full Sublattice of L holds not M_3 ,K are_isomorphic by Th10; :: thesis: verum

end;

assume for K being full Sublattice of L holds not M_3 ,K are_isomorphic ; :: thesis: L is distributive
then for a, b, c, d, e being Element of L holds
( not a <> b or not a <> c or not a <> d or not a <> e or not b <> c or not b <> d or not b <> e or not c <> d or not c <> e or not d <> e or not a "/\" b = a or not a "/\" c = a or not a "/\" d = a or not b "/\" e = b or not c "/\" e = c or not d "/\" e = d or not b "/\" c = a or not b "/\" d = a or not c "/\" d = a or not b "\/" c = e or not b "\/" d = e or not c "\/" d = e ) by Th10;
hence L is distributive by A1, Lm3; :: thesis: verum