:: YELLOW11 semantic presentation

theorem Th1: :: YELLOW11:1
3 = {0,1,2}
proof end;

theorem Th2: :: YELLOW11:2
2 \ 1 = {1}
proof end;

theorem Th3: :: YELLOW11:3
3 \ 1 = {1,2}
proof end;

theorem Th4: :: YELLOW11:4
3 \ 2 = {2}
proof end;

Lemma5: 3 \ 2 c= 3 \ 1
proof end;

theorem Th5: :: YELLOW11:5
for b1 being reflexive antisymmetric with_suprema with_infima RelStr
for b2, b3 being Element of b1 holds
( b2 "/\" b3 = b3 iff b2 "\/" b3 = b2 )
proof end;

theorem Th6: :: YELLOW11:6
for b1 being LATTICE
for b2, b3, b4 being Element of b1 holds (b2 "/\" b3) "\/" (b2 "/\" b4) <= b2 "/\" (b3 "\/" b4)
proof end;

theorem Th7: :: YELLOW11:7
for b1 being LATTICE
for b2, b3, b4 being Element of b1 holds b2 "\/" (b3 "/\" b4) <= (b2 "\/" b3) "/\" (b2 "\/" b4)
proof end;

theorem Th8: :: YELLOW11:8
for b1 being LATTICE
for b2, b3, b4 being Element of b1 st b2 <= b4 holds
b2 "\/" (b3 "/\" b4) <= (b2 "\/" b3) "/\" b4
proof end;

definition
func N_5 -> RelStr equals :: YELLOW11:def 1
 InclPoset {0,(3 \ 1),2,(3 \ 2),3};
correctness
coherence
InclPoset {0,(3 \ 1),2,(3 \ 2),3} is RelStr ;
;
end;

:: deftheorem Def1 defines N_5 YELLOW11:def 1 :
N_5 = InclPoset {0,(3 \ 1),2,(3 \ 2),3};

registration
cluster N_5 -> strict reflexive transitive antisymmetric ;
correctness
coherence
( N_5 is strict & N_5 is reflexive & N_5 is transitive & N_5 is antisymmetric );
;
cluster N_5 -> with_suprema with_infima ;
correctness
coherence
( N_5 is with_infima & N_5 is with_suprema );
proof end;
end;

definition
func M_3 -> RelStr equals :: YELLOW11:def 2
 InclPoset {0,1,(2 \ 1),(3 \ 2),3};
correctness
coherence
InclPoset {0,1,(2 \ 1),(3 \ 2),3} is RelStr ;
;
end;

:: deftheorem Def2 defines M_3 YELLOW11:def 2 :
M_3 = InclPoset {0,1,(2 \ 1),(3 \ 2),3};

registration
cluster M_3 -> strict reflexive transitive antisymmetric ;
correctness
coherence
( M_3 is strict & M_3 is reflexive & M_3 is transitive & M_3 is antisymmetric );
;
cluster M_3 -> with_suprema with_infima ;
correctness
coherence
( M_3 is with_infima & M_3 is with_suprema );
proof end;
end;

theorem Th9: :: YELLOW11:9
for b1 being LATTICE holds
( ex b2 being full Sublattice of b1 st N_5 ,b2 are_isomorphic iff ex b2, b3, b4, b5, b6 being Element of b1 st
( b2 <> b3 & b2 <> b4 & b2 <> b5 & b2 <> b6 & b3 <> b4 & b3 <> b5 & b3 <> b6 & b4 <> b5 & b4 <> b6 & b5 <> b6 & b2 "/\" b3 = b2 & b2 "/\" b4 = b2 & b4 "/\" b6 = b4 & b5 "/\" b6 = b5 & b3 "/\" b4 = b2 & b3 "/\" b5 = b3 & b4 "/\" b5 = b2 & b3 "\/" b4 = b6 & b4 "\/" b5 = b6 ) )
proof end;

theorem Th10: :: YELLOW11:10
for b1 being LATTICE holds
( ex b2 being full Sublattice of b1 st M_3 ,b2 are_isomorphic iff ex b2, b3, b4, b5, b6 being Element of b1 st
( b2 <> b3 & b2 <> b4 & b2 <> b5 & b2 <> b6 & b3 <> b4 & b3 <> b5 & b3 <> b6 & b4 <> b5 & b4 <> b6 & b5 <> b6 & b2 "/\" b3 = b2 & b2 "/\" b4 = b2 & b2 "/\" b5 = b2 & b3 "/\" b6 = b3 & b4 "/\" b6 = b4 & b5 "/\" b6 = b5 & b3 "/\" b4 = b2 & b3 "/\" b5 = b2 & b4 "/\" b5 = b2 & b3 "\/" b4 = b6 & b3 "\/" b5 = b6 & b4 "\/" b5 = b6 ) )
proof end;

definition
let c1 be non empty RelStr ;
attr a1 is modular means :Def3: :: YELLOW11:def 3
for b1, b2, b3 being Element of a1 st b1 <= b3 holds
b1 "\/" (b2 "/\" b3) = (b1 "\/" b2) "/\" b3;
end;

:: deftheorem Def3 defines modular YELLOW11:def 3 :
for b1 being non empty RelStr holds
( b1 is modular iff for b2, b3, b4 being Element of b1 st b2 <= b4 holds
b2 "\/" (b3 "/\" b4) = (b2 "\/" b3) "/\" b4 );

registration
cluster non empty reflexive antisymmetric with_infima distributive -> non empty reflexive antisymmetric with_infima modular RelStr ;
coherence
for b1 being non empty reflexive antisymmetric with_infima RelStr st b1 is distributive holds
b1 is modular
proof end;
end;

Lemma13: for b1 being LATTICE holds
( b1 is modular iff for b2, b3, b4, b5, b6 being Element of b1 holds
( not b2 <> b3 or not b2 <> b4 or not b2 <> b5 or not b2 <> b6 or not b3 <> b4 or not b3 <> b5 or not b3 <> b6 or not b4 <> b5 or not b4 <> b6 or not b5 <> b6 or not b2 "/\" b3 = b2 or not b2 "/\" b4 = b2 or not b4 "/\" b6 = b4 or not b5 "/\" b6 = b5 or not b3 "/\" b4 = b2 or not b3 "/\" b5 = b3 or not b4 "/\" b5 = b2 or not b3 "\/" b4 = b6 or not b4 "\/" b5 = b6 ) )
proof end;

theorem Th11: :: YELLOW11:11
for b1 being LATTICE holds
( b1 is modular iff for b2 being full Sublattice of b1 holds not N_5 ,b2 are_isomorphic )
proof end;

Lemma14: for b1 being LATTICE st b1 is modular holds
( b1 is distributive iff for b2, b3, b4, b5, b6 being Element of b1 holds
( not b2 <> b3 or not b2 <> b4 or not b2 <> b5 or not b2 <> b6 or not b3 <> b4 or not b3 <> b5 or not b3 <> b6 or not b4 <> b5 or not b4 <> b6 or not b5 <> b6 or not b2 "/\" b3 = b2 or not b2 "/\" b4 = b2 or not b2 "/\" b5 = b2 or not b3 "/\" b6 = b3 or not b4 "/\" b6 = b4 or not b5 "/\" b6 = b5 or not b3 "/\" b4 = b2 or not b3 "/\" b5 = b2 or not b4 "/\" b5 = b2 or not b3 "\/" b4 = b6 or not b3 "\/" b5 = b6 or not b4 "\/" b5 = b6 ) )
proof end;

theorem Th12: :: YELLOW11:12
for b1 being LATTICE st b1 is modular holds
( b1 is distributive iff for b2 being full Sublattice of b1 holds not M_3 ,b2 are_isomorphic )
proof end;

definition
let c1 be non empty RelStr ;
let c2, c3 be Element of c1;
func [#c2,c3#] -> Subset of a1 means :Def4: :: YELLOW11:def 4
for b1 being Element of a1 holds
( b1 in a4 iff ( a2 <= b1 & b1 <= a3 ) );
existence
ex b1 being Subset of c1 st
for b2 being Element of c1 holds
( b2 in b1 iff ( c2 <= b2 & b2 <= c3 ) )
proof end;
uniqueness
for b1, b2 being Subset of c1 st ( for b3 being Element of c1 holds
( b3 in b1 iff ( c2 <= b3 & b3 <= c3 ) ) ) & ( for b3 being Element of c1 holds
( b3 in b2 iff ( c2 <= b3 & b3 <= c3 ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def4 defines [# YELLOW11:def 4 :
for b1 being non empty RelStr
for b2, b3 being Element of b1
for b4 being Subset of b1 holds
( b4 = [#b2,b3#] iff for b5 being Element of b1 holds
( b5 in b4 iff ( b2 <= b5 & b5 <= b3 ) ) );

definition
let c1 be non empty RelStr ;
let c2 be Subset of c1;
attr a2 is interval means :Def5: :: YELLOW11:def 5
ex b1, b2 being Element of a1 st a2 = [#b1,b2#];
end;

:: deftheorem Def5 defines interval YELLOW11:def 5 :
for b1 being non empty RelStr
for b2 being Subset of b1 holds
( b2 is interval iff ex b3, b4 being Element of b1 st b2 = [#b3,b4#] );

registration
let c1 be non empty reflexive transitive RelStr ;
cluster non empty interval -> directed Element of K10(the carrier of a1);
coherence
for b1 being Subset of c1 st not b1 is empty & b1 is interval holds
b1 is directed
proof end;
cluster non empty interval -> filtered Element of K10(the carrier of a1);
coherence
for b1 being Subset of c1 st not b1 is empty & b1 is interval holds
b1 is filtered
proof end;
end;

registration
let c1 be non empty RelStr ;
let c2, c3 be Element of c1;
cluster [#a2,a3#] -> interval ;
coherence
[#c2,c3#] is interval by Def5;
end;

theorem Th13: :: YELLOW11:13
for b1 being non empty reflexive transitive RelStr
for b2, b3 being Element of b1 holds [#b2,b3#] = (uparrow b2) /\ (downarrow b3)
proof end;

registration
let c1 be with_infima Poset;
let c2, c3 be Element of c1;
cluster subrelstr [#a2,a3#] -> meet-inheriting ;
coherence
subrelstr [#c2,c3#] is meet-inheriting
proof end;
end;

registration
let c1 be with_suprema Poset;
let c2, c3 be Element of c1;
cluster subrelstr [#a2,a3#] -> join-inheriting ;
coherence
subrelstr [#c2,c3#] is join-inheriting
proof end;
end;

theorem Th14: :: YELLOW11:14
for b1 being LATTICE
for b2, b3 being Element of b1 st b1 is modular holds
subrelstr [#b3,(b2 "\/" b3)#], subrelstr [#(b2 "/\" b3),b2#] are_isomorphic
proof end;

registration
cluster non empty finite RelStr ;
existence
ex b1 being LATTICE st
( b1 is finite & not b1 is empty )
proof end;
end;

registration
cluster finite -> lower-bounded RelStr ;
coherence
for b1 being Semilattice st b1 is finite holds
b1 is lower-bounded
proof end;
end;

registration
cluster finite -> complete RelStr ;
coherence
for b1 being LATTICE st b1 is finite holds
b1 is complete
proof end;
end;