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 )

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

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
for K being full Sublattice of L holds not N_5 ,K are_isomorphic
; :: thesis: L is modular
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;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

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