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 :
N_5 = InclPoset {0,(3 \ 1),2,(3 \ 2),3};
:: deftheorem defines M_3 YELLOW11:def 2 :
M_3 = InclPoset {0,1,(2 \ 1),(3 \ 2),3};
theorem Th9:
theorem Th10:
begin
:: deftheorem Def3 defines modular YELLOW11:def 3 :
for L being non empty RelStr holds
( L is modular iff for a, b, c being Element of L st a <= c holds
a "\/" (b "/\" c) = (a "\/" b) "/\" c );
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 :
for L being non empty RelStr
for a, b being Element of L
for b4 being Subset of L holds
( b4 = [#a,b#] iff for c being Element of L holds
( c in b4 iff ( a <= c & c <= b ) ) );
:: deftheorem Def5 defines interval YELLOW11:def 5 :
for L being non empty RelStr
for IT being Subset of L holds
( IT is interval iff ex a, b being Element of L st IT = [#a,b#] );
theorem
theorem