:: MSUALG_2 semantic presentation

registration

let c₁ be set ;
let c₂ be ManySortedSet of c₁;
let c₃ be V6 ManySortedSet of c₁;
cluster a₂ \/ a₃ -> V6 ;
coherence

proof end;

cluster a₃ \/ a₂ -> V6 ;
coherence ;

end;

theorem Th1: :: MSUALG_2:1

canceled;

theorem Th2: :: MSUALG_2:2

for b₁ being non empty set
for b₂, b₃ being ManySortedSet of b₁
for b₄ being Element of b₁ * holds product ((b₂ /\ b₃) * b₄) = (product (b₂ * b₄)) /\ (product (b₃ * b₄))

proof end;

definition

let c₁ be non empty ManySortedSign ;
let c₂ be MSAlgebra of c₁;
mode MSSubset of a₂ is ManySortedSubset of the Sorts of a₂;

end;

definition

let c₁ be non empty ManySortedSign ;
let c₂ be SortSymbol of c₁;
canceled;
attr a₂ is with_const_op means :Def2: :: MSUALG_2:def 2
ex b₁ being OperSymbol of a₁ st
( the Arity of a₁ . b₁ = {} & the ResultSort of a₁ . b₁ = a₂ );

end;

:: deftheorem Def1 MSUALG_2:def 1 :

:: deftheorem Def2 defines with_const_op MSUALG_2:def 2 :

definition

let c₁ be non empty ManySortedSign ;
attr a₁ is all-with_const_op means :Def3: :: MSUALG_2:def 3
for b₁ being SortSymbol of a₁ holds b₁ is with_const_op;

end;

:: deftheorem Def3 defines all-with_const_op MSUALG_2:def 3 :

registration

let c₁ be non empty set ;
let c₂ be set ;
let c₃ be Function of c₂,c₁ * ;
let c₄ be Function of c₂,c₁;
cluster ManySortedSign(# a₁,a₂,a₃,a₄ #) -> non empty ;
coherence by STRUCT_0:def 1;

end;

registration

cluster non empty strict non void all-with_const_op ManySortedSign ;
existence

proof end;

end;

definition

let c₁ be non empty non void ManySortedSign ;
let c₂ be MSAlgebra of c₁;
let c₃ be SortSymbol of c₁;
func Constants c₂,c₃ -> Subset of (the Sorts of a₂ . a₃) means :Def4: :: MSUALG_2:def 4
ex b₁ being non empty set st
( b₁ = the Sorts of a₂ . a₃ & a₄ = { b₂ where B is Element of b₁ : ex b₁ being OperSymbol of a₁ st
( the Arity of a₁ . b₃ = {} & the ResultSort of a₁ . b₃ = a₃ & b₂ in rng (Den b₃,a₂) ) } ) if the Sorts of a₂ . a₃ <> {}
otherwise a₄ = {} ;
existence

proof end;

correctness ;

end;

:: deftheorem Def4 defines Constants MSUALG_2:def 4 :

definition

let c₁ be non empty non void ManySortedSign ;
let c₂ be MSAlgebra of c₁;
func Constants c₂ -> MSSubset of a₂ means :Def5: :: MSUALG_2:def 5
for b₁ being SortSymbol of a₁ holds a₃ . b₁ = Constants a₂,b₁;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines Constants MSUALG_2:def 5 :

registration

let c₁ be non empty non void all-with_const_op ManySortedSign ;
let c₂ be non-empty MSAlgebra of c₁;
let c₃ be SortSymbol of c₁;
cluster Constants a₂,a₃ -> non empty ;
coherence

proof end;

end;

registration

let c₁ be non empty non void all-with_const_op ManySortedSign ;
let c₂ be non-empty MSAlgebra of c₁;
cluster Constants a₂ -> V6 ;
coherence

proof end;

end;

definition

let c₁ be non empty non void ManySortedSign ;
let c₂ be MSAlgebra of c₁;
let c₃ be OperSymbol of c₁;
let c₄ be MSSubset of c₂;
pred c₄ is_closed_on c₃ means :Def6: :: MSUALG_2:def 6
rng ((Den a₃,a₂) | (((a₄ # ) * the Arity of a₁) . a₃)) c= (a₄ * the ResultSort of a₁) . a₃;

end;

:: deftheorem Def6 defines is_closed_on MSUALG_2:def 6 :

definition

let c₁ be non empty non void ManySortedSign ;
let c₂ be MSAlgebra of c₁;
let c₃ be MSSubset of c₂;
attr a₃ is opers_closed means :Def7: :: MSUALG_2:def 7
for b₁ being OperSymbol of a₁ holds a₃ is_closed_on b₁;

end;

:: deftheorem Def7 defines opers_closed MSUALG_2:def 7 :

theorem Th3: :: MSUALG_2:3

for b₁ being non empty non void ManySortedSign
for b₂ being OperSymbol of b₁
for b₃ being MSAlgebra of b₁
for b₄, b₅ being MSSubset of b₃ st b₄ c= b₅ holds
((b₄ # ) * the Arity of b₁) . b₂ c= ((b₅ # ) * the Arity of b₁) . b₂

proof end;

definition

let c₁ be non empty non void ManySortedSign ;
let c₂ be MSAlgebra of c₁;
let c₃ be OperSymbol of c₁;
let c₄ be MSSubset of c₂;
assume E9: c₄ is_closed_on c₃ ;
func c₃ /. c₄ -> Function of ((a₄ # ) * the Arity of a₁) . a₃,(a₄ * the ResultSort of a₁) . a₃ equals :Def8: :: MSUALG_2:def 8
(Den a₃,a₂) | (((a₄ # ) * the Arity of a₁) . a₃);
coherence

proof end;

end;

:: deftheorem Def8 defines /. MSUALG_2:def 8 :

definition

let c₁ be non empty non void ManySortedSign ;
let c₂ be MSAlgebra of c₁;
let c₃ be MSSubset of c₂;
func Opers c₂,c₃ -> ManySortedFunction of (a₃ # ) * the Arity of a₁,a₃ * the ResultSort of a₁ means :Def9: :: MSUALG_2:def 9
for b₁ being OperSymbol of a₁ holds a₄ . b₁ = b₁ /. a₃;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def9 defines Opers MSUALG_2:def 9 :

theorem Th4: :: MSUALG_2:4

for b₁ being non empty non void ManySortedSign
for b₂ being MSAlgebra of b₁
for b₃ being MSSubset of b₂ st b₃ = the Sorts of b₂ holds
( b₃ is opers_closed & ( for b₄ being OperSymbol of b₁ holds b₄ /. b₃ = Den b₄,b₂ ) )

proof end;

theorem Th5: :: MSUALG_2:5

for b₁ being non empty non void ManySortedSign
for b₂ being MSAlgebra of b₁
for b₃ being MSSubset of b₂ st b₃ = the Sorts of b₂ holds
Opers b₂,b₃ = the Charact of b₂

proof end;

definition

let c₁ be non empty non void ManySortedSign ;
let c₂ be MSAlgebra of c₁;
mode MSSubAlgebra of c₂ -> MSAlgebra of a₁ means :Def10: :: MSUALG_2:def 10
( the Sorts of a₃ is MSSubset of a₂ & ( for b₁ being MSSubset of a₂ st b₁ = the Sorts of a₃ holds
( b₁ is opers_closed & the Charact of a₃ = Opers a₂,b₁ ) ) );
existence

proof end;

end;

:: deftheorem Def10 defines MSSubAlgebra MSUALG_2:def 10 :

Lemma14: for b₁ being non empty non void ManySortedSign
for b₂ being MSAlgebra of b₁ holds MSAlgebra(# the Sorts of b₂,the Charact of b₂ #) is MSSubAlgebra of b₂

proof end;

registration

let c₁ be non empty non void ManySortedSign ;
let c₂ be MSAlgebra of c₁;
cluster strict MSSubAlgebra of a₂;
existence

proof end;

end;

registration

let c₁ be non empty non void ManySortedSign ;
let c₂ be non-empty MSAlgebra of c₁;
cluster MSAlgebra(# the Sorts of a₂,the Charact of a₂ #) -> non-empty ;
coherence by MSUALG_1:def 8;

end;

registration

let c₁ be non empty non void ManySortedSign ;
let c₂ be non-empty MSAlgebra of c₁;
cluster strict non-empty MSSubAlgebra of a₂;
existence

proof end;

end;

theorem Th6: :: MSUALG_2:6

for b₁ being non empty non void ManySortedSign
for b₂ being MSAlgebra of b₁ holds b₂ is MSSubAlgebra of b₂

proof end;

theorem Th7: :: MSUALG_2:7

for b₁ being non empty non void ManySortedSign
for b₂, b₃, b₄ being MSAlgebra of b₁ st b₂ is MSSubAlgebra of b₃ & b₃ is MSSubAlgebra of b₄ holds
b₂ is MSSubAlgebra of b₄

proof end;

theorem Th8: :: MSUALG_2:8

for b₁ being non empty non void ManySortedSign
for b₂, b₃ being MSAlgebra of b₁ st b₂ is strict MSSubAlgebra of b₃ & b₃ is strict MSSubAlgebra of b₂ holds
b₂ = b₃

proof end;

theorem Th9: :: MSUALG_2:9

for b₁ being non empty non void ManySortedSign
for b₂ being MSAlgebra of b₁
for b₃, b₄ being MSSubAlgebra of b₂ st the Sorts of b₃ c= the Sorts of b₄ holds
b₃ is MSSubAlgebra of b₄

proof end;

theorem Th10: :: MSUALG_2:10

for b₁ being non empty non void ManySortedSign
for b₂ being MSAlgebra of b₁
for b₃, b₄ being strict MSSubAlgebra of b₂ st the Sorts of b₃ = the Sorts of b₄ holds
b₃ = b₄

proof end;

theorem Th11: :: MSUALG_2:11

for b₁ being non empty non void ManySortedSign
for b₂ being MSAlgebra of b₁
for b₃ being MSSubAlgebra of b₂ holds Constants b₂ is MSSubset of b₃

proof end;

theorem Th12: :: MSUALG_2:12

for b₁ being non empty non void all-with_const_op ManySortedSign
for b₂ being non-empty MSAlgebra of b₁
for b₃ being non-empty MSSubAlgebra of b₂ holds Constants b₂ is V6 MSSubset of b₃ by Th11;

theorem Th13: :: MSUALG_2:13

for b₁ being non empty non void all-with_const_op ManySortedSign
for b₂ being non-empty MSAlgebra of b₁
for b₃, b₄ being non-empty MSSubAlgebra of b₂ holds the Sorts of b₃ /\ the Sorts of b₄ is non-empty

proof end;

definition

let c₁ be non empty non void ManySortedSign ;
let c₂ be MSAlgebra of c₁;
let c₃ be MSSubset of c₂;
func SubSort c₃ -> set means :Def11: :: MSUALG_2:def 11
for b₁ being set holds
( b₁ in a₄ iff ( b₁ in Funcs the carrier of a₁,(bool (Union the Sorts of a₂)) & b₁ is MSSubset of a₂ & ( for b₂ being MSSubset of a₂ st b₂ = b₁ holds
( b₂ is opers_closed & Constants a₂ c= b₂ & a₃ c= b₂ ) ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def11 defines SubSort MSUALG_2:def 11 :

Lemma20: for b₁ being non empty non void ManySortedSign
for b₂ being MSAlgebra of b₁
for b₃ being MSSubset of b₂ holds the Sorts of b₂ in SubSort b₃

proof end;

registration

let c₁ be non empty non void ManySortedSign ;
let c₂ be MSAlgebra of c₁;
let c₃ be MSSubset of c₂;
cluster SubSort a₃ -> non empty ;
coherence by Lemma20;

end;

definition

let c₁ be non empty non void ManySortedSign ;
let c₂ be MSAlgebra of c₁;
func SubSort c₂ -> set means :Def12: :: MSUALG_2:def 12
for b₁ being set holds
( b₁ in a₃ iff ( b₁ in Funcs the carrier of a₁,(bool (Union the Sorts of a₂)) & b₁ is MSSubset of a₂ & ( for b₂ being MSSubset of a₂ st b₂ = b₁ holds
b₂ is opers_closed ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def12 defines SubSort MSUALG_2:def 12 :

registration

let c₁ be non empty non void ManySortedSign ;
let c₂ be MSAlgebra of c₁;
cluster SubSort a₂ -> non empty ;
coherence

proof end;

end;

definition

let c₁ be non empty non void ManySortedSign ;
let c₂ be MSAlgebra of c₁;
let c₃ be Element of SubSort c₂;
func @ c₃ -> MSSubset of a₂ equals :: MSUALG_2:def 13
a₃;
coherence by Def12;

end;

:: deftheorem Def13 defines @ MSUALG_2:def 13 :

theorem Th14: :: MSUALG_2:14

for b₁ being non empty non void ManySortedSign
for b₂ being MSAlgebra of b₁
for b₃, b₄ being MSSubset of b₂ holds
( b₄ in SubSort b₃ iff ( b₄ is opers_closed & Constants b₂ c= b₄ & b₃ c= b₄ ) )

proof end;

theorem Th15: :: MSUALG_2:15

for b₁ being non empty non void ManySortedSign
for b₂ being MSAlgebra of b₁
for b₃ being MSSubset of b₂ holds
( b₃ in SubSort b₂ iff b₃ is opers_closed )

proof end;

definition

let c₁ be non empty non void ManySortedSign ;
let c₂ be MSAlgebra of c₁;
let c₃ be MSSubset of c₂;
let c₄ be SortSymbol of c₁;
func SubSort c₃,c₄ -> set means :Def14: :: MSUALG_2:def 14
for b₁ being set holds
( b₁ in a₅ iff ex b₂ being MSSubset of a₂ st
( b₂ in SubSort a₃ & b₁ = b₂ . a₄ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def14 defines SubSort MSUALG_2:def 14 :

registration

let c₁ be non empty non void ManySortedSign ;
let c₂ be MSAlgebra of c₁;
let c₃ be MSSubset of c₂;
let c₄ be SortSymbol of c₁;
cluster SubSort a₃,a₄ -> non empty ;
coherence

proof end;

end;

definition

let c₁ be non empty non void ManySortedSign ;
let c₂ be MSAlgebra of c₁;
let c₃ be MSSubset of c₂;
func MSSubSort c₃ -> MSSubset of a₂ means :Def15: :: MSUALG_2:def 15
for b₁ being SortSymbol of a₁ holds a₄ . b₁ = meet (SubSort a₃,b₁);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def15 defines MSSubSort MSUALG_2:def 15 :

theorem Th16: :: MSUALG_2:16

for b₁ being non empty non void ManySortedSign
for b₂ being MSAlgebra of b₁
for b₃ being MSSubset of b₂ holds (Constants b₂) \/ b₃ c= MSSubSort b₃

proof end;

theorem Th17: :: MSUALG_2:17

for b₁ being non empty non void ManySortedSign
for b₂ being MSAlgebra of b₁
for b₃ being MSSubset of b₂ st (Constants b₂) \/ b₃ is non-empty holds
MSSubSort b₃ is non-empty

proof end;

theorem Th18: :: MSUALG_2:18

for b₁ being non empty non void ManySortedSign
for b₂ being OperSymbol of b₁
for b₃ being MSAlgebra of b₁
for b₄, b₅ being MSSubset of b₃ st b₅ in SubSort b₄ holds
(((MSSubSort b₄) # ) * the Arity of b₁) . b₂ c= ((b₅ # ) * the Arity of b₁) . b₂

proof end;

theorem Th19: :: MSUALG_2:19

for b₁ being non empty non void ManySortedSign
for b₂ being OperSymbol of b₁
for b₃ being MSAlgebra of b₁
for b₄, b₅ being MSSubset of b₃ st b₅ in SubSort b₄ holds
rng ((Den b₂,b₃) | ((((MSSubSort b₄) # ) * the Arity of b₁) . b₂)) c= (b₅ * the ResultSort of b₁) . b₂

proof end;

theorem Th20: :: MSUALG_2:20

for b₁ being non empty non void ManySortedSign
for b₂ being OperSymbol of b₁
for b₃ being MSAlgebra of b₁
for b₄ being MSSubset of b₃ holds rng ((Den b₂,b₃) | ((((MSSubSort b₄) # ) * the Arity of b₁) . b₂)) c= ((MSSubSort b₄) * the ResultSort of b₁) . b₂

proof end;

theorem Th21: :: MSUALG_2:21

for b₁ being non empty non void ManySortedSign
for b₂ being MSAlgebra of b₁
for b₃ being MSSubset of b₂ holds
( MSSubSort b₃ is opers_closed & b₃ c= MSSubSort b₃ )

proof end;

definition

let c₁ be non empty non void ManySortedSign ;
let c₂ be MSAlgebra of c₁;
let c₃ be MSSubset of c₂;
assume E32: c₃ is opers_closed ;
func c₂ | c₃ -> strict MSSubAlgebra of a₂ equals :Def16: :: MSUALG_2:def 16
MSAlgebra(# a₃,(Opers a₂,a₃) #);
coherence

proof end;

end;

:: deftheorem Def16 defines | MSUALG_2:def 16 :

definition

let c₁ be non empty non void ManySortedSign ;
let c₂ be MSAlgebra of c₁;
let c₃, c₄ be MSSubAlgebra of c₂;
func c₃ /\ c₄ -> strict MSSubAlgebra of a₂ means :Def17: :: MSUALG_2:def 17
( the Sorts of a₅ = the Sorts of a₃ /\ the Sorts of a₄ & ( for b₁ being MSSubset of a₂ st b₁ = the Sorts of a₅ holds
( b₁ is opers_closed & the Charact of a₅ = Opers a₂,b₁ ) ) );
existence

proof end;

uniqueness by Th10;

end;

:: deftheorem Def17 defines /\ MSUALG_2:def 17 :

definition

let c₁ be non empty non void ManySortedSign ;
let c₂ be MSAlgebra of c₁;
let c₃ be MSSubset of c₂;
func GenMSAlg c₃ -> strict MSSubAlgebra of a₂ means :Def18: :: MSUALG_2:def 18
( a₃ is MSSubset of a₄ & ( for b₁ being MSSubAlgebra of a₂ st a₃ is MSSubset of b₁ holds
a₄ is MSSubAlgebra of b₁ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def18 defines GenMSAlg MSUALG_2:def 18 :

registration

let c₁ be non empty non void ManySortedSign ;
let c₂ be non-empty MSAlgebra of c₁;
let c₃ be V6 MSSubset of c₂;
cluster GenMSAlg a₃ -> strict non-empty ;
coherence

proof end;

end;

theorem Th22: :: MSUALG_2:22

for b₁ being non empty non void ManySortedSign
for b₂ being strict MSAlgebra of b₁
for b₃ being MSSubset of b₂ st b₃ = the Sorts of b₂ holds
GenMSAlg b₃ = b₂

proof end;

theorem Th23: :: MSUALG_2:23

for b₁ being non empty non void ManySortedSign
for b₂ being MSAlgebra of b₁
for b₃ being strict MSSubAlgebra of b₂
for b₄ being MSSubset of b₂ st b₄ = the Sorts of b₃ holds
GenMSAlg b₄ = b₃

proof end;

theorem Th24: :: MSUALG_2:24

for b₁ being non empty non void ManySortedSign
for b₂ being non-empty MSAlgebra of b₁
for b₃ being MSSubAlgebra of b₂ holds (GenMSAlg (Constants b₂)) /\ b₃ = GenMSAlg (Constants b₂)

proof end;

definition

let c₁ be non empty non void ManySortedSign ;
let c₂ be non-empty MSAlgebra of c₁;
let c₃, c₄ be MSSubAlgebra of c₂;
func c₃ "\/" c₄ -> strict MSSubAlgebra of a₂ means :Def19: :: MSUALG_2:def 19
for b₁ being MSSubset of a₂ st b₁ = the Sorts of a₃ \/ the Sorts of a₄ holds
a₅ = GenMSAlg b₁;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def19 defines "\/" MSUALG_2:def 19 :

theorem Th25: :: MSUALG_2:25

for b₁ being non empty non void ManySortedSign
for b₂ being non-empty MSAlgebra of b₁
for b₃ being MSSubAlgebra of b₂
for b₄, b₅ being MSSubset of b₂ st b₅ = b₄ \/ the Sorts of b₃ holds
(GenMSAlg b₄) "\/" b₃ = GenMSAlg b₅

proof end;

theorem Th26: :: MSUALG_2:26

for b₁ being non empty non void ManySortedSign
for b₂ being non-empty MSAlgebra of b₁
for b₃ being MSSubAlgebra of b₂
for b₄ being MSSubset of b₂ st b₄ = the Sorts of b₂ holds
(GenMSAlg b₄) "\/" b₃ = GenMSAlg b₄

proof end;

theorem Th27: :: MSUALG_2:27

for b₁ being non empty non void ManySortedSign
for b₂ being non-empty MSAlgebra of b₁
for b₃, b₄ being MSSubAlgebra of b₂ holds b₃ "\/" b₄ = b₄ "\/" b₃

proof end;

theorem Th28: :: MSUALG_2:28

for b₁ being non empty non void ManySortedSign
for b₂ being non-empty MSAlgebra of b₁
for b₃, b₄ being strict MSSubAlgebra of b₂ holds b₃ /\ (b₃ "\/" b₄) = b₃

proof end;

theorem Th29: :: MSUALG_2:29

for b₁ being non empty non void ManySortedSign
for b₂ being non-empty MSAlgebra of b₁
for b₃, b₄ being strict MSSubAlgebra of b₂ holds (b₃ /\ b₄) "\/" b₄ = b₄

proof end;

definition

let c₁ be non empty non void ManySortedSign ;
let c₂ be MSAlgebra of c₁;
func MSSub c₂ -> set means :Def20: :: MSUALG_2:def 20
for b₁ being set holds
( b₁ in a₃ iff b₁ is strict MSSubAlgebra of a₂ );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def20 defines MSSub MSUALG_2:def 20 :

registration

let c₁ be non empty non void ManySortedSign ;
let c₂ be MSAlgebra of c₁;
cluster MSSub a₂ -> non empty ;
coherence

proof end;

end;

definition

let c₁ be non empty non void ManySortedSign ;
let c₂ be non-empty MSAlgebra of c₁;
func MSAlg_join c₂ -> BinOp of MSSub a₂ means :Def21: :: MSUALG_2:def 21
for b₁, b₂ being Element of MSSub a₂
for b₃, b₄ being strict MSSubAlgebra of a₂ st b₁ = b₃ & b₂ = b₄ holds
a₃ . b₁,b₂ = b₃ "\/" b₄;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def21 defines MSAlg_join MSUALG_2:def 21 :

definition

let c₁ be non empty non void ManySortedSign ;
let c₂ be non-empty MSAlgebra of c₁;
func MSAlg_meet c₂ -> BinOp of MSSub a₂ means :Def22: :: MSUALG_2:def 22
for b₁, b₂ being Element of MSSub a₂
for b₃, b₄ being strict MSSubAlgebra of a₂ st b₁ = b₃ & b₂ = b₄ holds
a₃ . b₁,b₂ = b₃ /\ b₄;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def22 defines MSAlg_meet MSUALG_2:def 22 :

theorem Th30: :: MSUALG_2:30

for b₁ being non empty non void ManySortedSign
for b₂ being non-empty MSAlgebra of b₁ holds MSAlg_join b₂ is commutative

proof end;

theorem Th31: :: MSUALG_2:31

for b₁ being non empty non void ManySortedSign
for b₂ being non-empty MSAlgebra of b₁ holds MSAlg_join b₂ is associative

proof end;

theorem Th32: :: MSUALG_2:32

for b₁ being non empty non void ManySortedSign
for b₂ being non-empty MSAlgebra of b₁ holds MSAlg_meet b₂ is commutative

proof end;

theorem Th33: :: MSUALG_2:33

for b₁ being non empty non void ManySortedSign
for b₂ being non-empty MSAlgebra of b₁ holds MSAlg_meet b₂ is associative

proof end;

definition

let c₁ be non empty non void ManySortedSign ;
let c₂ be non-empty MSAlgebra of c₁;
func MSSubAlLattice c₂ -> strict Lattice equals :: MSUALG_2:def 23
LattStr(# (MSSub a₂),(MSAlg_join a₂),(MSAlg_meet a₂) #);
coherence

proof end;

end;

:: deftheorem Def23 defines MSSubAlLattice MSUALG_2:def 23 :

theorem Th34: :: MSUALG_2:34

for b₁ being non empty non void ManySortedSign
for b₂ being non-empty MSAlgebra of b₁ holds MSSubAlLattice b₂ is bounded

proof end;

registration

let c₁ be non empty non void ManySortedSign ;
let c₂ be non-empty MSAlgebra of c₁;
cluster MSSubAlLattice a₂ -> strict bounded ;
coherence by Th34;

end;

theorem Th35: :: MSUALG_2:35

for b₁ being non empty non void ManySortedSign
for b₂ being non-empty MSAlgebra of b₁ holds Bottom (MSSubAlLattice b₂) = GenMSAlg (Constants b₂)

proof end;

theorem Th36: :: MSUALG_2:36

for b₁ being non empty non void ManySortedSign
for b₂ being non-empty MSAlgebra of b₁
for b₃ being MSSubset of b₂ st b₃ = the Sorts of b₂ holds
Top (MSSubAlLattice b₂) = GenMSAlg b₃

proof end;

theorem Th37: :: MSUALG_2:37

for b₁ being non empty non void ManySortedSign
for b₂ being strict non-empty MSAlgebra of b₁ holds Top (MSSubAlLattice b₂) = b₂

proof end;

theorem Th38: :: MSUALG_2:38

for b₁ being non empty non void ManySortedSign
for b₂ being MSAlgebra of b₁ holds MSAlgebra(# the Sorts of b₂,the Charact of b₂ #) is MSSubAlgebra of b₂ by Lemma14;

theorem Th39: :: MSUALG_2:39

canceled;

theorem Th40: :: MSUALG_2:40

for b₁ being non empty non void ManySortedSign
for b₂ being MSAlgebra of b₁
for b₃ being MSSubset of b₂ holds the Sorts of b₂ in SubSort b₃ by Lemma20;

theorem Th41: :: MSUALG_2:41

for b₁ being non empty non void ManySortedSign
for b₂ being MSAlgebra of b₁
for b₃ being MSSubset of b₂ holds SubSort b₃ c= SubSort b₂

proof end;