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 )

then for a, b, c, d, e being Element of L holds

( not a,b,c,d,e are_mutually_distinct 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

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
for K being full Sublattice of L holds not M_3 ,K are_isomorphic
; :: thesis: L is distributive
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,c,d,e are_mutually_distinct 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;then for a, b, c, d, e being Element of L holds

( not a,b,c,d,e are_mutually_distinct 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

then for a, b, c, d, e being Element of L holds

( not a,b,c,d,e are_mutually_distinct 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