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

proof

assume L is modular ; :: thesis: for K being full Sublattice of L holds not N_5 ,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 c "/\" e = c or not d "/\" e = d or not b "/\" c = a or not b "/\" d = b or not c "/\" d = a or not b "\/" c = e or not c "\/" d = e ) by Lm2;
hence for K being full Sublattice of L holds not N_5 ,K are_isomorphic by Th9; :: thesis: verum

end;

assume for K being full Sublattice of L holds not N_5 ,K are_isomorphic ; :: thesis: L is modular
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 c "/\" e = c or not d "/\" e = d or not b "/\" c = a or not b "/\" d = b or not c "/\" d = a or not b "\/" c = e or not c "\/" d = e ) by Th9;
hence L is modular by Lm2; :: thesis: verum