:: OSALG_2 semantic presentation

theorem Th1: :: OSALG_2:1

for b₁ being non empty Poset
for b₂, b₃ being OrderSortedSet of b₁ holds b₂ /\ b₃ is OrderSortedSet of b₁

proof end;

theorem Th2: :: OSALG_2:2

for b₁ being non empty Poset
for b₂, b₃ being OrderSortedSet of b₁ holds b₂ \/ b₃ is OrderSortedSet of b₁

proof end;

definition

let c₁ be non empty Poset;
let c₂ be OrderSortedSet of c₁;
mode OrderSortedSubset of c₂ -> ManySortedSubset of a₂ means :Def1: :: OSALG_2:def 1
a₃ is OrderSortedSet of a₁;
existence

proof end;

end;

:: deftheorem Def1 defines OrderSortedSubset OSALG_2:def 1 :

registration

let c₁ be non empty Poset;
let c₂ be V3 OrderSortedSet of c₁;
cluster V3 OrderSortedSubset of a₂;
existence

proof end;

end;

definition

let c₁ be OrderSortedSign;
let c₂ be OSAlgebra of c₁;
mode OSSubset of c₂ -> ManySortedSubset of the Sorts of a₂ means :Def2: :: OSALG_2:def 2
a₃ is OrderSortedSet of a₁;
existence

proof end;

end;

:: deftheorem Def2 defines OSSubset OSALG_2:def 2 :

registration

let c₁ be OrderSortedSign;
cluster strict non-empty monotone MSAlgebra of a₁;
existence

proof end;

end;

registration

let c₁ be OrderSortedSign;
let c₂ be non-empty OSAlgebra of c₁;
cluster V3 OSSubset of a₂;
existence

proof end;

end;

theorem Th3: :: OSALG_2:3

for b₁ being non empty strict non void all-with_const_op ManySortedSign holds OSSign b₁ is all-with_const_op

proof end;

registration

cluster strict all-with_const_op OverloadedRSSign ;
existence

proof end;

end;

theorem Th4: :: OSALG_2:4

for b₁ being OrderSortedSign
for b₂ being OSAlgebra of b₁ holds MSAlgebra(# the Sorts of b₂,the Charact of b₂ #) is order-sorted

proof end;

registration

let c₁ be OrderSortedSign;
let c₂ be OSAlgebra of c₁;
cluster order-sorted MSSubAlgebra of a₂;
existence

proof end;

end;

definition

let c₁ be OrderSortedSign;
let c₂ be OSAlgebra of c₁;
mode OSSubAlgebra of a₂ is order-sorted MSSubAlgebra of a₂;

end;

registration

let c₁ be OrderSortedSign;
let c₂ be OSAlgebra of c₁;
cluster strict MSSubAlgebra of a₂;
existence

proof end;

end;

registration

let c₁ be OrderSortedSign;
let c₂ be non-empty OSAlgebra of c₁;
cluster strict non-empty MSSubAlgebra of a₂;
existence

proof end;

end;

theorem Th5: :: OSALG_2:5

for b₁ being OrderSortedSign
for b₂ being OSAlgebra of b₁
for b₃ being MSAlgebra of b₁ holds
( b₃ is OSSubAlgebra of b₂ iff ( the Sorts of b₃ is OSSubset of b₂ & ( for b₄ being OSSubset of b₂ st b₄ = the Sorts of b₃ holds
( b₄ is opers_closed & the Charact of b₃ = Opers b₂,b₄ ) ) ) )

proof end;

definition

let c₁ be OrderSortedSign;
let c₂ be OSAlgebra of c₁;
let c₃ be SortSymbol of c₁;
func OSConstants c₂,c₃ -> Subset of (the Sorts of a₂ . a₃) equals :: OSALG_2:def 3
union { (Constants a₂,b₁) where B is SortSymbol of a₁ : b₁ <= a₃ } ;
coherence

proof end;

end;

:: deftheorem Def3 defines OSConstants OSALG_2:def 3 :

theorem Th6: :: OSALG_2:6

canceled;

theorem Th7: :: OSALG_2:7

canceled;

theorem Th8: :: OSALG_2:8

canceled;

theorem Th9: :: OSALG_2:9

canceled;

theorem Th10: :: OSALG_2:10

canceled;

theorem Th11: :: OSALG_2:11

for b₁ being OrderSortedSign
for b₂ being OSAlgebra of b₁
for b₃ being SortSymbol of b₁ holds Constants b₂,b₃ c= OSConstants b₂,b₃

proof end;

definition

let c₁ be OrderSortedSign;
let c₂ be ManySortedSet of the carrier of c₁;
func OSCl c₂ -> OrderSortedSet of a₁ means :Def4: :: OSALG_2:def 4
for b₁ being SortSymbol of a₁ holds a₃ . b₁ = union { (a₂ . b₂) where B is SortSymbol of a₁ : b₂ <= b₁ } ;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines OSCl OSALG_2:def 4 :

theorem Th12: :: OSALG_2:12

for b₁ being OrderSortedSign
for b₂ being ManySortedSet of the carrier of b₁ holds b₂ c= OSCl b₂

proof end;

theorem Th13: :: OSALG_2:13

for b₁ being OrderSortedSign
for b₂ being ManySortedSet of the carrier of b₁
for b₃ being OrderSortedSet of b₁ st b₂ c= b₃ holds
OSCl b₂ c= b₃

proof end;

theorem Th14: :: OSALG_2:14

for b₁ being OrderSortedSign
for b₂ being OrderSortedSet of b₁ holds OSCl b₂ = b₂

proof end;

definition

let c₁ be OrderSortedSign;
let c₂ be OSAlgebra of c₁;
func OSConstants c₂ -> OSSubset of a₂ means :Def5: :: OSALG_2:def 5
for b₁ being SortSymbol of a₁ holds a₃ . b₁ = OSConstants a₂,b₁;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines OSConstants OSALG_2:def 5 :

theorem Th15: :: OSALG_2:15

for b₁ being OrderSortedSign
for b₂ being OSAlgebra of b₁ holds Constants b₂ c= OSConstants b₂

proof end;

theorem Th16: :: OSALG_2:16

for b₁ being OrderSortedSign
for b₂ being OSAlgebra of b₁
for b₃ being OSSubset of b₂ st Constants b₂ c= b₃ holds
OSConstants b₂ c= b₃

proof end;

theorem Th17: :: OSALG_2:17

for b₁ being OrderSortedSign
for b₂ being OSAlgebra of b₁
for b₃ being OSSubset of b₂ holds OSConstants b₂ = OSCl (Constants b₂)

proof end;

theorem Th18: :: OSALG_2:18

for b₁ being OrderSortedSign
for b₂ being OSAlgebra of b₁
for b₃ being OSSubAlgebra of b₂ holds OSConstants b₂ is OSSubset of b₃

proof end;

theorem Th19: :: OSALG_2:19

for b₁ being all-with_const_op OrderSortedSign
for b₂ being non-empty OSAlgebra of b₁
for b₃ being non-empty OSSubAlgebra of b₂ holds OSConstants b₂ is V3 OSSubset of b₃

proof end;

theorem Th20: :: OSALG_2:20

for b₁ being set
for b₂ being ManySortedSet of b₁
for b₃ being set holds
( b₃ is ManySortedSubset of b₂ iff b₃ in product (bool b₂) )

proof end;

definition

let c₁ be non empty Poset;
let c₂ be OrderSortedSet of c₁;
func OSbool c₂ -> set means :: OSALG_2:def 6
for b₁ being set holds
( b₁ in a₃ iff b₁ is OrderSortedSubset of a₂ );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def6 defines OSbool OSALG_2:def 6 :

definition

let c₁ be OrderSortedSign;
let c₂ be OSAlgebra of c₁;
let c₃ be OSSubset of c₂;
func OSSubSort c₃ -> set equals :: OSALG_2:def 7
{ b₁ where B is Element of SubSort a₃ : b₁ is OrderSortedSet of a₁ } ;
correctness ;

end;

:: deftheorem Def7 defines OSSubSort OSALG_2:def 7 :

theorem Th21: :: OSALG_2:21

for b₁ being OrderSortedSign
for b₂ being OSAlgebra of b₁
for b₃ being OSSubset of b₂ holds OSSubSort b₃ c= SubSort b₃

proof end;

theorem Th22: :: OSALG_2:22

for b₁ being OrderSortedSign
for b₂ being OSAlgebra of b₁
for b₃ being OSSubset of b₂ holds the Sorts of b₂ in OSSubSort b₃

proof end;

registration

let c₁ be OrderSortedSign;
let c₂ be OSAlgebra of c₁;
let c₃ be OSSubset of c₂;
cluster OSSubSort a₃ -> non empty ;
coherence by Th22;

end;

definition

let c₁ be OrderSortedSign;
let c₂ be OSAlgebra of c₁;
func OSSubSort c₂ -> set equals :: OSALG_2:def 8
{ b₁ where B is Element of SubSort a₂ : b₁ is OrderSortedSet of a₁ } ;
correctness ;

end;

:: deftheorem Def8 defines OSSubSort OSALG_2:def 8 :

theorem Th23: :: OSALG_2:23

for b₁ being OrderSortedSign
for b₂ being OSAlgebra of b₁
for b₃ being OSSubset of b₂ holds OSSubSort b₃ c= OSSubSort b₂

proof end;

registration

let c₁ be OrderSortedSign;
let c₂ be OSAlgebra of c₁;
cluster OSSubSort a₂ -> non empty ;
coherence

proof end;

end;

definition

let c₁ be OrderSortedSign;
let c₂ be OSAlgebra of c₁;
let c₃ be Element of OSSubSort c₂;
func @ c₃ -> OSSubset of a₂ equals :: OSALG_2:def 9
a₃;
coherence

proof end;

end;

:: deftheorem Def9 defines @ OSALG_2:def 9 :

theorem Th24: :: OSALG_2:24

for b₁ being OrderSortedSign
for b₂ being OSAlgebra of b₁
for b₃, b₄ being OSSubset of b₂ holds
( b₄ in OSSubSort b₃ iff ( b₄ is opers_closed & OSConstants b₂ c= b₄ & b₃ c= b₄ ) )

proof end;

theorem Th25: :: OSALG_2:25

for b₁ being OrderSortedSign
for b₂ being OSAlgebra of b₁
for b₃ being OSSubset of b₂ holds
( b₃ in OSSubSort b₂ iff b₃ is opers_closed )

proof end;

definition

let c₁ be OrderSortedSign;
let c₂ be OSAlgebra of c₁;
let c₃ be OSSubset of c₂;
let c₄ be Element of c₁;
func OSSubSort c₃,c₄ -> set means :Def10: :: OSALG_2:def 10
for b₁ being set holds
( b₁ in a₅ iff ex b₂ being OSSubset of a₂ st
( b₂ in OSSubSort a₃ & b₁ = b₂ . a₄ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def10 defines OSSubSort OSALG_2:def 10 :

theorem Th26: :: OSALG_2:26

for b₁ being OrderSortedSign
for b₂ being OSAlgebra of b₁
for b₃ being OSSubset of b₂
for b₄, b₅ being SortSymbol of b₁ st b₄ <= b₅ holds
OSSubSort b₃,b₅ is_coarser_than OSSubSort b₃,b₄

proof end;

theorem Th27: :: OSALG_2:27

for b₁ being OrderSortedSign
for b₂ being OSAlgebra of b₁
for b₃ being OSSubset of b₂
for b₄ being SortSymbol of b₁ holds OSSubSort b₃,b₄ c= SubSort b₃,b₄

proof end;

theorem Th28: :: OSALG_2:28

for b₁ being OrderSortedSign
for b₂ being OSAlgebra of b₁
for b₃ being OSSubset of b₂
for b₄ being SortSymbol of b₁ holds the Sorts of b₂ . b₄ in OSSubSort b₃,b₄

proof end;

registration

let c₁ be OrderSortedSign;
let c₂ be OSAlgebra of c₁;
let c₃ be OSSubset of c₂;
let c₄ be SortSymbol of c₁;
cluster OSSubSort a₃,a₄ -> non empty ;
coherence by Th28;

end;

definition

let c₁ be OrderSortedSign;
let c₂ be OSAlgebra of c₁;
let c₃ be OSSubset of c₂;
func OSMSubSort c₃ -> OSSubset of a₂ means :Def11: :: OSALG_2:def 11
for b₁ being SortSymbol of a₁ holds a₄ . b₁ = meet (OSSubSort a₃,b₁);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def11 defines OSMSubSort OSALG_2:def 11 :

registration

let c₁ be OrderSortedSign;
let c₂ be OSAlgebra of c₁;
cluster opers_closed OSSubset of a₂;
existence

proof end;

end;

theorem Th29: :: OSALG_2:29

for b₁ being OrderSortedSign
for b₂ being OSAlgebra of b₁
for b₃ being OSSubset of b₂ holds (OSConstants b₂) \/ b₃ c= OSMSubSort b₃

proof end;

theorem Th30: :: OSALG_2:30

for b₁ being OrderSortedSign
for b₂ being OSAlgebra of b₁
for b₃ being OSSubset of b₂ st (OSConstants b₂) \/ b₃ is non-empty holds
OSMSubSort b₃ is non-empty

proof end;

theorem Th31: :: OSALG_2:31

for b₁ being OrderSortedSign
for b₂ being OSAlgebra of b₁
for b₃ being OperSymbol of b₁
for b₄, b₅ being OSSubset of b₂ st b₅ in OSSubSort b₄ holds
(((OSMSubSort b₄) # ) * the Arity of b₁) . b₃ c= ((b₅ # ) * the Arity of b₁) . b₃

proof end;

theorem Th32: :: OSALG_2:32

for b₁ being OrderSortedSign
for b₂ being OSAlgebra of b₁
for b₃ being OperSymbol of b₁
for b₄, b₅ being OSSubset of b₂ st b₅ in OSSubSort b₄ holds
rng ((Den b₃,b₂) | ((((OSMSubSort b₄) # ) * the Arity of b₁) . b₃)) c= (b₅ * the ResultSort of b₁) . b₃

proof end;

theorem Th33: :: OSALG_2:33

for b₁ being OrderSortedSign
for b₂ being OSAlgebra of b₁
for b₃ being OperSymbol of b₁
for b₄ being OSSubset of b₂ holds rng ((Den b₃,b₂) | ((((OSMSubSort b₄) # ) * the Arity of b₁) . b₃)) c= ((OSMSubSort b₄) * the ResultSort of b₁) . b₃

proof end;

theorem Th34: :: OSALG_2:34

for b₁ being OrderSortedSign
for b₂ being OSAlgebra of b₁
for b₃ being OSSubset of b₂ holds
( OSMSubSort b₃ is opers_closed & b₃ c= OSMSubSort b₃ )

proof end;

registration

let c₁ be OrderSortedSign;
let c₂ be OSAlgebra of c₁;
let c₃ be OSSubset of c₂;
cluster OSMSubSort a₃ -> opers_closed ;
coherence by Th34;

end;

registration

let c₁ be OrderSortedSign;
let c₂ be OSAlgebra of c₁;
let c₃ be opers_closed OSSubset of c₂;
cluster a₂ | a₃ -> order-sorted ;
coherence

proof end;

end;

registration

let c₁ be OrderSortedSign;
let c₂ be OSAlgebra of c₁;
let c₃, c₄ be OSSubAlgebra of c₂;
cluster a₃ /\ a₄ -> order-sorted ;
coherence

proof end;

end;

definition

let c₁ be OrderSortedSign;
let c₂ be OSAlgebra of c₁;
let c₃ be OSSubset of c₂;
canceled;
func GenOSAlg c₃ -> strict OSSubAlgebra of a₂ means :Def13: :: OSALG_2:def 13
( a₃ is OSSubset of a₄ & ( for b₁ being OSSubAlgebra of a₂ st a₃ is OSSubset of b₁ holds
a₄ is OSSubAlgebra of b₁ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def12 OSALG_2:def 12 :

:: deftheorem Def13 defines GenOSAlg OSALG_2:def 13 :

theorem Th35: :: OSALG_2:35

for b₁ being OrderSortedSign
for b₂ being OSAlgebra of b₁
for b₃ being OSSubset of b₂ holds
( GenOSAlg b₃ = b₂ | (OSMSubSort b₃) & the Sorts of (GenOSAlg b₃) = OSMSubSort b₃ )

proof end;

theorem Th36: :: OSALG_2:36

for b₁ being non empty non void ManySortedSign
for b₂ being MSAlgebra of b₁
for b₃ being MSSubset of b₂ holds
( GenMSAlg b₃ = b₂ | (MSSubSort b₃) & the Sorts of (GenMSAlg b₃) = MSSubSort b₃ )

proof end;

theorem Th37: :: OSALG_2:37

for b₁ being OrderSortedSign
for b₂ being OSAlgebra of b₁
for b₃ being OSSubset of b₂ holds the Sorts of (GenMSAlg b₃) c= the Sorts of (GenOSAlg b₃)

proof end;

theorem Th38: :: OSALG_2:38

for b₁ being OrderSortedSign
for b₂ being OSAlgebra of b₁
for b₃ being OSSubset of b₂ holds GenMSAlg b₃ is MSSubAlgebra of GenOSAlg b₃

proof end;

theorem Th39: :: OSALG_2:39

for b₁ being OrderSortedSign
for b₂ being strict OSAlgebra of b₁
for b₃ being OSSubset of b₂ st b₃ = the Sorts of b₂ holds
GenOSAlg b₃ = b₂

proof end;

theorem Th40: :: OSALG_2:40

for b₁ being OrderSortedSign
for b₂ being OSAlgebra of b₁
for b₃ being strict OSSubAlgebra of b₂
for b₄ being OSSubset of b₂ st b₄ = the Sorts of b₃ holds
GenOSAlg b₄ = b₃

proof end;

theorem Th41: :: OSALG_2:41

for b₁ being OrderSortedSign
for b₂ being non-empty OSAlgebra of b₁
for b₃ being OSSubAlgebra of b₂ holds (GenOSAlg (OSConstants b₂)) /\ b₃ = GenOSAlg (OSConstants b₂)

proof end;

definition

let c₁ be OrderSortedSign;
let c₂ be non-empty OSAlgebra of c₁;
let c₃, c₄ be OSSubAlgebra of c₂;
func c₃ "\/"_os c₄ -> strict OSSubAlgebra of a₂ means :Def14: :: OSALG_2:def 14
for b₁ being OSSubset of a₂ st b₁ = the Sorts of a₃ \/ the Sorts of a₄ holds
a₅ = GenOSAlg b₁;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def14 defines "\/"_os OSALG_2:def 14 :

theorem Th42: :: OSALG_2:42

for b₁ being OrderSortedSign
for b₂ being non-empty OSAlgebra of b₁
for b₃ being OSSubAlgebra of b₂
for b₄, b₅ being OSSubset of b₂ st b₅ = b₄ \/ the Sorts of b₃ holds
(GenOSAlg b₄) "\/"_os b₃ = GenOSAlg b₅

proof end;

theorem Th43: :: OSALG_2:43

for b₁ being OrderSortedSign
for b₂ being non-empty OSAlgebra of b₁
for b₃ being OSSubAlgebra of b₂
for b₄ being OSSubset of b₂ st b₄ = the Sorts of b₂ holds
(GenOSAlg b₄) "\/"_os b₃ = GenOSAlg b₄

proof end;

theorem Th44: :: OSALG_2:44

for b₁ being OrderSortedSign
for b₂ being non-empty OSAlgebra of b₁
for b₃, b₄ being OSSubAlgebra of b₂ holds b₃ "\/"_os b₄ = b₄ "\/"_os b₃

proof end;

theorem Th45: :: OSALG_2:45

for b₁ being OrderSortedSign
for b₂ being non-empty OSAlgebra of b₁
for b₃, b₄ being strict OSSubAlgebra of b₂ holds b₃ /\ (b₃ "\/"_os b₄) = b₃

proof end;

theorem Th46: :: OSALG_2:46

for b₁ being OrderSortedSign
for b₂ being non-empty OSAlgebra of b₁
for b₃, b₄ being strict OSSubAlgebra of b₂ holds (b₃ /\ b₄) "\/"_os b₄ = b₄

proof end;

definition

let c₁ be OrderSortedSign;
let c₂ be OSAlgebra of c₁;
func OSSub c₂ -> set means :Def15: :: OSALG_2:def 15
for b₁ being set holds
( b₁ in a₃ iff b₁ is strict OSSubAlgebra of a₂ );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def15 defines OSSub OSALG_2:def 15 :

theorem Th47: :: OSALG_2:47

for b₁ being OrderSortedSign
for b₂ being OSAlgebra of b₁ holds OSSub b₂ c= MSSub b₂

proof end;

registration

let c₁ be OrderSortedSign;
let c₂ be OSAlgebra of c₁;
cluster OSSub a₂ -> non empty ;
coherence

proof end;

end;

definition

let c₁ be OrderSortedSign;
let c₂ be OSAlgebra of c₁;
redefine func OSSub as OSSub c₂ -> Subset of (MSSub a₂);
coherence by Th47;

end;

definition

let c₁ be OrderSortedSign;
let c₂ be non-empty OSAlgebra of c₁;
func OSAlg_join c₂ -> BinOp of OSSub a₂ means :Def16: :: OSALG_2:def 16
for b₁, b₂ being Element of OSSub a₂
for b₃, b₄ being strict OSSubAlgebra of a₂ st b₁ = b₃ & b₂ = b₄ holds
a₃ . b₁,b₂ = b₃ "\/"_os b₄;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def16 defines OSAlg_join OSALG_2:def 16 :

definition

let c₁ be OrderSortedSign;
let c₂ be non-empty OSAlgebra of c₁;
func OSAlg_meet c₂ -> BinOp of OSSub a₂ means :Def17: :: OSALG_2:def 17
for b₁, b₂ being Element of OSSub a₂
for b₃, b₄ being strict OSSubAlgebra of a₂ st b₁ = b₃ & b₂ = b₄ holds
a₃ . b₁,b₂ = b₃ /\ b₄;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def17 defines OSAlg_meet OSALG_2:def 17 :

theorem Th48: :: OSALG_2:48

for b₁ being OrderSortedSign
for b₂ being non-empty OSAlgebra of b₁
for b₃, b₄ being Element of OSSub b₂ holds (OSAlg_meet b₂) . b₃,b₄ = (MSAlg_meet b₂) . b₃,b₄

proof end;

theorem Th49: :: OSALG_2:49

for b₁ being OrderSortedSign
for b₂ being non-empty OSAlgebra of b₁ holds OSAlg_join b₂ is commutative

proof end;

theorem Th50: :: OSALG_2:50

for b₁ being OrderSortedSign
for b₂ being non-empty OSAlgebra of b₁ holds OSAlg_join b₂ is associative

proof end;

theorem Th51: :: OSALG_2:51

for b₁ being OrderSortedSign
for b₂ being non-empty OSAlgebra of b₁ holds OSAlg_meet b₂ is commutative

proof end;

theorem Th52: :: OSALG_2:52

for b₁ being OrderSortedSign
for b₂ being non-empty OSAlgebra of b₁ holds OSAlg_meet b₂ is associative

proof end;

definition

let c₁ be OrderSortedSign;
let c₂ be non-empty OSAlgebra of c₁;
func OSSubAlLattice c₂ -> strict Lattice equals :: OSALG_2:def 18
LattStr(# (OSSub a₂),(OSAlg_join a₂),(OSAlg_meet a₂) #);
coherence

proof end;

end;

:: deftheorem Def18 defines OSSubAlLattice OSALG_2:def 18 :

theorem Th53: :: OSALG_2:53

for b₁ being OrderSortedSign
for b₂ being non-empty OSAlgebra of b₁ holds OSSubAlLattice b₂ is bounded

proof end;

registration

let c₁ be OrderSortedSign;
let c₂ be non-empty OSAlgebra of c₁;
cluster OSSubAlLattice a₂ -> strict bounded ;
coherence by Th53;

end;

theorem Th54: :: OSALG_2:54

for b₁ being OrderSortedSign
for b₂ being non-empty OSAlgebra of b₁ holds Bottom (OSSubAlLattice b₂) = GenOSAlg (OSConstants b₂)

proof end;

theorem Th55: :: OSALG_2:55

for b₁ being OrderSortedSign
for b₂ being non-empty OSAlgebra of b₁
for b₃ being OSSubset of b₂ st b₃ = the Sorts of b₂ holds
Top (OSSubAlLattice b₂) = GenOSAlg b₃

proof end;

theorem Th56: :: OSALG_2:56

for b₁ being OrderSortedSign
for b₂ being strict non-empty OSAlgebra of b₁ holds Top (OSSubAlLattice b₂) = b₂

proof end;