:: MSUALG_7 semantic presentation

theorem Th1: :: MSUALG_7:1
for b1, b2 being set holds
( b1 in the carrier of (EqRelLatt b2) iff b1 is Equivalence_Relation of b2 )
proof end;

theorem Th2: :: MSUALG_7:2
for b1 being non empty set
for b2 being ManySortedSet of b1 holds id b2 is Equivalence_Relation of b2
proof end;

theorem Th3: :: MSUALG_7:3
for b1 being non empty set
for b2 being ManySortedSet of b1 holds [|b2,b2|] is Equivalence_Relation of b2
proof end;

registration
let c1 be non empty set ;
let c2 be ManySortedSet of c1;
cluster EqRelLatt a2 -> bounded ;
coherence
EqRelLatt c2 is bounded
proof end;
end;

theorem Th4: :: MSUALG_7:4
for b1 being non empty set
for b2 being ManySortedSet of b1 holds Bottom (EqRelLatt b2) = id b2
proof end;

theorem Th5: :: MSUALG_7:5
for b1 being non empty set
for b2 being ManySortedSet of b1 holds Top (EqRelLatt b2) = [|b2,b2|]
proof end;

theorem Th6: :: MSUALG_7:6
for b1 being non empty set
for b2 being ManySortedSet of b1
for b3 being Subset of (EqRelLatt b2) holds b3 is SubsetFamily of [|b2,b2|]
proof end;

theorem Th7: :: MSUALG_7:7
for b1 being non empty set
for b2 being ManySortedSet of b1
for b3, b4 being Element of (EqRelLatt b2)
for b5, b6 being Equivalence_Relation of b2 st b3 = b5 & b4 = b6 holds
( b3 [= b4 iff b5 c= b6 )
proof end;

theorem Th8: :: MSUALG_7:8
for b1 being non empty set
for b2 being ManySortedSet of b1
for b3 being Subset of (EqRelLatt b2)
for b4 being SubsetFamily of [|b2,b2|] st b4 = b3 holds
for b5, b6 being Equivalence_Relation of b2 st b5 = meet |:b4:| & b6 in b3 holds
b5 c= b6
proof end;

theorem Th9: :: MSUALG_7:9
for b1 being non empty set
for b2 being ManySortedSet of b1
for b3 being Subset of (EqRelLatt b2)
for b4 being SubsetFamily of [|b2,b2|] st b4 = b3 & not b3 is empty holds
meet |:b4:| is Equivalence_Relation of b2
proof end;

definition
let c1 be non empty LattStr ;
redefine attr a1 is complete means :Def1: :: MSUALG_7:def 1
for b1 being Subset of a1 ex b2 being Element of a1 st
( b1 is_less_than b2 & ( for b3 being Element of a1 st b1 is_less_than b3 holds
b2 [= b3 ) );
compatibility
( c1 is complete iff for b1 being Subset of c1 ex b2 being Element of c1 st
( b1 is_less_than b2 & ( for b3 being Element of c1 st b1 is_less_than b3 holds
b2 [= b3 ) ) )
proof end;
end;

:: deftheorem Def1 defines complete MSUALG_7:def 1 :
for b1 being non empty LattStr holds
( b1 is complete iff for b2 being Subset of b1 ex b3 being Element of b1 st
( b2 is_less_than b3 & ( for b4 being Element of b1 st b2 is_less_than b4 holds
b3 [= b4 ) ) );

theorem Th10: :: MSUALG_7:10
for b1 being non empty set
for b2 being ManySortedSet of b1 holds EqRelLatt b2 is complete
proof end;

registration
let c1 be non empty set ;
let c2 be ManySortedSet of c1;
cluster EqRelLatt a2 -> bounded complete ;
coherence
EqRelLatt c2 is complete by Th10;
end;

theorem Th11: :: MSUALG_7:11
for b1 being non empty set
for b2 being ManySortedSet of b1
for b3 being Subset of (EqRelLatt b2)
for b4 being SubsetFamily of [|b2,b2|] st b4 = b3 & not b3 is empty holds
for b5, b6 being Equivalence_Relation of b2 st b5 = meet |:b4:| & b6 = "/\" b3,(EqRelLatt b2) holds
b5 = b6
proof end;

definition
let c1 be Lattice;
let c2 be SubLattice of c1;
attr a2 is /\-inheriting means :Def2: :: MSUALG_7:def 2
for b1 being Subset of a2 holds "/\" b1,a1 in the carrier of a2;
attr a2 is \/-inheriting means :Def3: :: MSUALG_7:def 3
for b1 being Subset of a2 holds "\/" b1,a1 in the carrier of a2;
end;

:: deftheorem Def2 defines /\-inheriting MSUALG_7:def 2 :
for b1 being Lattice
for b2 being SubLattice of b1 holds
( b2 is /\-inheriting iff for b3 being Subset of b2 holds "/\" b3,b1 in the carrier of b2 );

:: deftheorem Def3 defines \/-inheriting MSUALG_7:def 3 :
for b1 being Lattice
for b2 being SubLattice of b1 holds
( b2 is \/-inheriting iff for b3 being Subset of b2 holds "\/" b3,b1 in the carrier of b2 );

theorem Th12: :: MSUALG_7:12
for b1 being Lattice
for b2 being SubLattice of b1
for b3, b4 being Element of b1
for b5, b6 being Element of b2 st b3 = b5 & b4 = b6 holds
( b3 "\/" b4 = b5 "\/" b6 & b3 "/\" b4 = b5 "/\" b6 )
proof end;

theorem Th13: :: MSUALG_7:13
for b1 being Lattice
for b2 being SubLattice of b1
for b3 being Subset of b2
for b4 being Element of b1
for b5 being Element of b2 st b4 = b5 holds
( b4 is_less_than b3 iff b5 is_less_than b3 )
proof end;

theorem Th14: :: MSUALG_7:14
for b1 being Lattice
for b2 being SubLattice of b1
for b3 being Subset of b2
for b4 being Element of b1
for b5 being Element of b2 st b4 = b5 holds
( b3 is_less_than b4 iff b3 is_less_than b5 )
proof end;

theorem Th15: :: MSUALG_7:15
for b1 being complete Lattice
for b2 being SubLattice of b1 st b2 is /\-inheriting holds
b2 is complete
proof end;

theorem Th16: :: MSUALG_7:16
for b1 being complete Lattice
for b2 being SubLattice of b1 st b2 is \/-inheriting holds
b2 is complete
proof end;

registration
let c1 be complete Lattice;
cluster complete SubLattice of a1;
existence
ex b1 being SubLattice of c1 st b1 is complete
proof end;
end;

registration
let c1 be complete Lattice;
cluster /\-inheriting -> complete SubLattice of a1;
coherence
for b1 being SubLattice of c1 st b1 is /\-inheriting holds
b1 is complete by Th15;
cluster \/-inheriting -> complete SubLattice of a1;
coherence
for b1 being SubLattice of c1 st b1 is \/-inheriting holds
b1 is complete by Th16;
end;

theorem Th17: :: MSUALG_7:17
for b1 being complete Lattice
for b2 being SubLattice of b1 st b2 is /\-inheriting holds
for b3 being Subset of b2 holds "/\" b3,b1 = "/\" b3,b2
proof end;

theorem Th18: :: MSUALG_7:18
for b1 being complete Lattice
for b2 being SubLattice of b1 st b2 is \/-inheriting holds
for b3 being Subset of b2 holds "\/" b3,b1 = "\/" b3,b2
proof end;

theorem Th19: :: MSUALG_7:19
for b1 being complete Lattice
for b2 being SubLattice of b1 st b2 is /\-inheriting holds
for b3 being Subset of b1
for b4 being Subset of b2 st b3 = b4 holds
"/\" b3 = "/\" b4 by Th17;

theorem Th20: :: MSUALG_7:20
for b1 being complete Lattice
for b2 being SubLattice of b1 st b2 is \/-inheriting holds
for b3 being Subset of b1
for b4 being Subset of b2 st b3 = b4 holds
"\/" b3 = "\/" b4 by Th18;

definition
let c1, c2 be Real;
assume E18: c1 <= c2 ;
func RealSubLatt c1,c2 -> strict Lattice means :Def4: :: MSUALG_7:def 4
( the carrier of a3 = [.a1,a2.] & the L_join of a3 = maxreal || [.a1,a2.] & the L_meet of a3 = minreal || [.a1,a2.] );
existence
ex b1 being strict Lattice st
( the carrier of b1 = [.c1,c2.] & the L_join of b1 = maxreal || [.c1,c2.] & the L_meet of b1 = minreal || [.c1,c2.] )
proof end;
uniqueness
for b1, b2 being strict Lattice st the carrier of b1 = [.c1,c2.] & the L_join of b1 = maxreal || [.c1,c2.] & the L_meet of b1 = minreal || [.c1,c2.] & the carrier of b2 = [.c1,c2.] & the L_join of b2 = maxreal || [.c1,c2.] & the L_meet of b2 = minreal || [.c1,c2.] holds
b1 = b2 ;
end;

:: deftheorem Def4 defines RealSubLatt MSUALG_7:def 4 :
for b1, b2 being Real st b1 <= b2 holds
for b3 being strict Lattice holds
( b3 = RealSubLatt b1,b2 iff ( the carrier of b3 = [.b1,b2.] & the L_join of b3 = maxreal || [.b1,b2.] & the L_meet of b3 = minreal || [.b1,b2.] ) );

theorem Th21: :: MSUALG_7:21
for b1, b2 being Real st b1 <= b2 holds
RealSubLatt b1,b2 is complete
proof end;

theorem Th22: :: MSUALG_7:22
ex b1 being SubLattice of RealSubLatt 0,1 st
( b1 is \/-inheriting & not b1 is /\-inheriting )
proof end;

theorem Th23: :: MSUALG_7:23
ex b1 being complete Latticeex b2 being SubLattice of b1 st
( b2 is \/-inheriting & not b2 is /\-inheriting )
proof end;

theorem Th24: :: MSUALG_7:24
ex b1 being SubLattice of RealSubLatt 0,1 st
( b1 is /\-inheriting & not b1 is \/-inheriting )
proof end;

theorem Th25: :: MSUALG_7:25
ex b1 being complete Latticeex b2 being SubLattice of b1 st
( b2 is /\-inheriting & not b2 is \/-inheriting )
proof end;