begin
theorem
theorem Th2:
theorem Th3:
theorem Th4:
Lm1:
3 \ 2 c= 3 \ 1
begin
theorem Th5:
theorem Th6:
theorem Th7:
theorem Th8:
:: deftheorem defines N_5 YELLOW11:def 1 :
:: deftheorem defines M_3 YELLOW11:def 2 :
theorem Th9:
theorem Th10:
begin
:: deftheorem Def3 defines modular YELLOW11:def 3 :
Lm2:
for L being LATTICE holds
( L is modular iff 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 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 ) )
theorem
Lm3:
for L being LATTICE st L is modular holds
( L is distributive iff 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 ) )
theorem
begin
:: deftheorem Def4 defines [# YELLOW11:def 4 :
:: deftheorem Def5 defines interval YELLOW11:def 5 :
theorem
theorem