:: by Josef Urban

::

:: Received September 19, 2002

:: Copyright (c) 2002-2017 Association of Mizar Users

:: should be clusters, but that requires redef of the operation

theorem Th1: :: OSALG_2:1

for R being non empty Poset

for X, Y being OrderSortedSet of R holds X (/\) Y is OrderSortedSet of R

for X, Y being OrderSortedSet of R holds X (/\) Y is OrderSortedSet of R

proof end;

theorem Th2: :: OSALG_2:2

for R being non empty Poset

for X, Y being OrderSortedSet of R holds X (\/) Y is OrderSortedSet of R

for X, Y being OrderSortedSet of R holds X (\/) Y is OrderSortedSet of R

proof end;

:: new and bad

definition

let R be non empty Poset;

let M be OrderSortedSet of R;

ex b_{1} being ManySortedSubset of M st b_{1} is OrderSortedSet of R

end;
let M be OrderSortedSet of R;

mode OrderSortedSubset of M -> ManySortedSubset of M means :Def1: :: OSALG_2:def 1

it is OrderSortedSet of R;

existence it is OrderSortedSet of R;

ex b

proof end;

:: deftheorem Def1 defines OrderSortedSubset OSALG_2:def 1 :

for R being non empty Poset

for M being OrderSortedSet of R

for b_{3} being ManySortedSubset of M holds

( b_{3} is OrderSortedSubset of M iff b_{3} is OrderSortedSet of R );

for R being non empty Poset

for M being OrderSortedSet of R

for b

( b

registration

let R be non empty Poset;

let M be V8() OrderSortedSet of R;

not for b_{1} being OrderSortedSubset of M holds b_{1} is V8()

end;
let M be V8() OrderSortedSet of R;

cluster non empty Relation-like V8() the carrier of R -defined Function-like V17( the carrier of R) for OrderSortedSubset of M;

existence not for b

proof end;

::

:: Constants of an Order Sorted Algebra.

::

:: Constants of an Order Sorted Algebra.

::

definition

let S be OrderSortedSign;

let U0 be OSAlgebra of S;

ex b_{1} being ManySortedSubset of the Sorts of U0 st b_{1} is OrderSortedSet of S

end;
let U0 be OSAlgebra of S;

mode OSSubset of U0 -> ManySortedSubset of the Sorts of U0 means :Def2: :: OSALG_2:def 2

it is OrderSortedSet of S;

existence it is OrderSortedSet of S;

ex b

proof end;

:: deftheorem Def2 defines OSSubset OSALG_2:def 2 :

for S being OrderSortedSign

for U0 being OSAlgebra of S

for b_{3} being ManySortedSubset of the Sorts of U0 holds

( b_{3} is OSSubset of U0 iff b_{3} is OrderSortedSet of S );

for S being OrderSortedSign

for U0 being OSAlgebra of S

for b

( b

:: very strange, the cluster in OSALG_1 should take care of this one

registration

let S be OrderSortedSign;

existence

ex b_{1} being OSAlgebra of S st

( b_{1} is monotone & b_{1} is strict & b_{1} is non-empty )

end;
existence

ex b

( b

proof end;

registration

let S be OrderSortedSign;

let U0 be non-empty OSAlgebra of S;

not for b_{1} being OSSubset of U0 holds b_{1} is V8()

end;
let U0 be non-empty OSAlgebra of S;

cluster non empty Relation-like V8() the carrier of S -defined Function-like V17( the carrier of S) for OSSubset of U0;

existence not for b

proof end;

theorem Th3: :: OSALG_2:3

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

proof end;

registration

ex b_{1} being OrderSortedSign st

( b_{1} is all-with_const_op & b_{1} is strict )
end;

cluster non empty non void V55() all-with_const_op V110() V111() V112() strict order-sorted discernable for OverloadedRSSign ;

existence ex b

( b

proof end;

::

:: Subalgebras of a Order Sorted Algebra.

::

:: Subalgebras of a Order Sorted Algebra.

::

theorem Th4: :: OSALG_2:4

for S being OrderSortedSign

for U0 being OSAlgebra of S holds MSAlgebra(# the Sorts of U0, the Charact of U0 #) is order-sorted

for U0 being OSAlgebra of S holds MSAlgebra(# the Sorts of U0, the Charact of U0 #) is order-sorted

proof end;

registration

let S be OrderSortedSign;

let U0 be OSAlgebra of S;

existence

ex b_{1} being MSSubAlgebra of U0 st b_{1} is order-sorted

end;
let U0 be OSAlgebra of S;

existence

ex b

proof end;

definition

let S be OrderSortedSign;

let U0 be OSAlgebra of S;

mode OSSubAlgebra of U0 is order-sorted MSSubAlgebra of U0;

end;
let U0 be OSAlgebra of S;

mode OSSubAlgebra of U0 is order-sorted MSSubAlgebra of U0;

registration

let S be OrderSortedSign;

let U0 be OSAlgebra of S;

existence

ex b_{1} being OSSubAlgebra of U0 st b_{1} is strict

end;
let U0 be OSAlgebra of S;

existence

ex b

proof end;

registration

let S be OrderSortedSign;

let U0 be non-empty OSAlgebra of S;

existence

ex b_{1} being OSSubAlgebra of U0 st

( b_{1} is non-empty & b_{1} is strict )

end;
let U0 be non-empty OSAlgebra of S;

existence

ex b

( b

proof end;

:: the equivalent def, maybe not needed

theorem Th5: :: OSALG_2:5

for S being OrderSortedSign

for U0 being OSAlgebra of S

for U1 being MSAlgebra over S holds

( U1 is OSSubAlgebra of U0 iff ( the Sorts of U1 is OSSubset of U0 & ( for B being OSSubset of U0 st B = the Sorts of U1 holds

( B is opers_closed & the Charact of U1 = Opers (U0,B) ) ) ) )

for U0 being OSAlgebra of S

for U1 being MSAlgebra over S holds

( U1 is OSSubAlgebra of U0 iff ( the Sorts of U1 is OSSubset of U0 & ( for B being OSSubset of U0 st B = the Sorts of U1 holds

( B is opers_closed & the Charact of U1 = Opers (U0,B) ) ) ) )

proof end;

definition

let S1 be OrderSortedSign;

let OU0 be OSAlgebra of S1;

let s be SortSymbol of S1;

union { (Constants (OU0,s2)) where s2 is SortSymbol of S1 : s2 <= s } is Subset of ( the Sorts of OU0 . s)

end;
let OU0 be OSAlgebra of S1;

let s be SortSymbol of S1;

func OSConstants (OU0,s) -> Subset of ( the Sorts of OU0 . s) equals :: OSALG_2:def 3

union { (Constants (OU0,s2)) where s2 is SortSymbol of S1 : s2 <= s } ;

coherence union { (Constants (OU0,s2)) where s2 is SortSymbol of S1 : s2 <= s } ;

union { (Constants (OU0,s2)) where s2 is SortSymbol of S1 : s2 <= s } is Subset of ( the Sorts of OU0 . s)

proof end;

:: deftheorem defines OSConstants OSALG_2:def 3 :

for S1 being OrderSortedSign

for OU0 being OSAlgebra of S1

for s being SortSymbol of S1 holds OSConstants (OU0,s) = union { (Constants (OU0,s2)) where s2 is SortSymbol of S1 : s2 <= s } ;

for S1 being OrderSortedSign

for OU0 being OSAlgebra of S1

for s being SortSymbol of S1 holds OSConstants (OU0,s) = union { (Constants (OU0,s2)) where s2 is SortSymbol of S1 : s2 <= s } ;

:: maybe

:: theorem S1 is discrete implies OSConstants(OU0,s) = Constants(OU0,s);

:: theorem S1 is discrete implies OSConstants(OU0,s) = Constants(OU0,s);

theorem Th6: :: OSALG_2:6

for S1 being OrderSortedSign

for OU0 being OSAlgebra of S1

for s being SortSymbol of S1 holds Constants (OU0,s) c= OSConstants (OU0,s)

for OU0 being OSAlgebra of S1

for s being SortSymbol of S1 holds Constants (OU0,s) c= OSConstants (OU0,s)

proof end;

definition

let S1 be OrderSortedSign;

let M be ManySortedSet of the carrier of S1;

ex b_{1} being OrderSortedSet of S1 st

for s being SortSymbol of S1 holds b_{1} . s = union { (M . s1) where s1 is SortSymbol of S1 : s1 <= s }

for b_{1}, b_{2} being OrderSortedSet of S1 st ( for s being SortSymbol of S1 holds b_{1} . s = union { (M . s1) where s1 is SortSymbol of S1 : s1 <= s } ) & ( for s being SortSymbol of S1 holds b_{2} . s = union { (M . s1) where s1 is SortSymbol of S1 : s1 <= s } ) holds

b_{1} = b_{2}

end;
let M be ManySortedSet of the carrier of S1;

func OSCl M -> OrderSortedSet of S1 means :Def4: :: OSALG_2:def 4

for s being SortSymbol of S1 holds it . s = union { (M . s1) where s1 is SortSymbol of S1 : s1 <= s } ;

existence for s being SortSymbol of S1 holds it . s = union { (M . s1) where s1 is SortSymbol of S1 : s1 <= s } ;

ex b

for s being SortSymbol of S1 holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def4 defines OSCl OSALG_2:def 4 :

for S1 being OrderSortedSign

for M being ManySortedSet of the carrier of S1

for b_{3} being OrderSortedSet of S1 holds

( b_{3} = OSCl M iff for s being SortSymbol of S1 holds b_{3} . s = union { (M . s1) where s1 is SortSymbol of S1 : s1 <= s } );

for S1 being OrderSortedSign

for M being ManySortedSet of the carrier of S1

for b

( b

theorem Th8: :: OSALG_2:8

for S1 being OrderSortedSign

for M being ManySortedSet of the carrier of S1

for A being OrderSortedSet of S1 st M c= A holds

OSCl M c= A

for M being ManySortedSet of the carrier of S1

for A being OrderSortedSet of S1 st M c= A holds

OSCl M c= A

proof end;

:: following should be rewritten to use OSCl Constants(OU0) instead;

:: maybe later

:: maybe later

definition

let S1 be OrderSortedSign;

let OU0 be OSAlgebra of S1;

ex b_{1} being OSSubset of OU0 st

for s being SortSymbol of S1 holds b_{1} . s = OSConstants (OU0,s)

for b_{1}, b_{2} being OSSubset of OU0 st ( for s being SortSymbol of S1 holds b_{1} . s = OSConstants (OU0,s) ) & ( for s being SortSymbol of S1 holds b_{2} . s = OSConstants (OU0,s) ) holds

b_{1} = b_{2}

end;
let OU0 be OSAlgebra of S1;

func OSConstants OU0 -> OSSubset of OU0 means :Def5: :: OSALG_2:def 5

for s being SortSymbol of S1 holds it . s = OSConstants (OU0,s);

existence for s being SortSymbol of S1 holds it . s = OSConstants (OU0,s);

ex b

for s being SortSymbol of S1 holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def5 defines OSConstants OSALG_2:def 5 :

for S1 being OrderSortedSign

for OU0 being OSAlgebra of S1

for b_{3} being OSSubset of OU0 holds

( b_{3} = OSConstants OU0 iff for s being SortSymbol of S1 holds b_{3} . s = OSConstants (OU0,s) );

for S1 being OrderSortedSign

for OU0 being OSAlgebra of S1

for b

( b

theorem Th11: :: OSALG_2:11

for S1 being OrderSortedSign

for OU0 being OSAlgebra of S1

for A being OSSubset of OU0 st Constants OU0 c= A holds

OSConstants OU0 c= A

for OU0 being OSAlgebra of S1

for A being OSSubset of OU0 st Constants OU0 c= A holds

OSConstants OU0 c= A

proof end;

theorem :: OSALG_2:12

for S1 being OrderSortedSign

for OU0 being OSAlgebra of S1

for A being OSSubset of OU0 holds OSConstants OU0 = OSCl (Constants OU0)

for OU0 being OSAlgebra of S1

for A being OSSubset of OU0 holds OSConstants OU0 = OSCl (Constants OU0)

proof end;

theorem Th13: :: OSALG_2:13

for S1 being OrderSortedSign

for OU0 being OSAlgebra of S1

for OU1 being OSSubAlgebra of OU0 holds OSConstants OU0 is OSSubset of OU1

for OU0 being OSAlgebra of S1

for OU1 being OSSubAlgebra of OU0 holds OSConstants OU0 is OSSubset of OU1

proof end;

theorem :: OSALG_2:14

for S being all-with_const_op OrderSortedSign

for OU0 being non-empty OSAlgebra of S

for OU1 being non-empty OSSubAlgebra of OU0 holds OSConstants OU0 is V8() OSSubset of OU1

for OU0 being non-empty OSAlgebra of S

for OU1 being non-empty OSSubAlgebra of OU0 holds OSConstants OU0 is V8() OSSubset of OU1

proof end;

::

:: Order Sorted Subsets of an Order Sorted Algebra.

::

:: this should be in MSUALG_2

:: Order Sorted Subsets of an Order Sorted Algebra.

::

:: this should be in MSUALG_2

theorem Th15: :: OSALG_2:15

for I being set

for M being ManySortedSet of I

for x being set holds

( x is ManySortedSubset of M iff x in product (bool M) )

for M being ManySortedSet of I

for x being set holds

( x is ManySortedSubset of M iff x in product (bool M) )

proof end;

:: Fraenkel should be improved, to allow more than just Element type

definition

let R be non empty Poset;

let M be OrderSortedSet of R;

ex b_{1} being set st

for x being set holds

( x in b_{1} iff x is OrderSortedSubset of M )

for b_{1}, b_{2} being set st ( for x being set holds

( x in b_{1} iff x is OrderSortedSubset of M ) ) & ( for x being set holds

( x in b_{2} iff x is OrderSortedSubset of M ) ) holds

b_{1} = b_{2}

end;
let M be OrderSortedSet of R;

func OSbool M -> set means :: OSALG_2:def 6

for x being set holds

( x in it iff x is OrderSortedSubset of M );

existence for x being set holds

( x in it iff x is OrderSortedSubset of M );

ex b

for x being set holds

( x in b

proof end;

uniqueness for b

( x in b

( x in b

b

proof end;

:: deftheorem defines OSbool OSALG_2:def 6 :

for R being non empty Poset

for M being OrderSortedSet of R

for b_{3} being set holds

( b_{3} = OSbool M iff for x being set holds

( x in b_{3} iff x is OrderSortedSubset of M ) );

for R being non empty Poset

for M being OrderSortedSet of R

for b

( b

( x in b

definition

let S be OrderSortedSign;

let U0 be OSAlgebra of S;

let A be OSSubset of U0;

coherence

{ x where x is Element of SubSort A : x is OrderSortedSet of S } is set ;

;

end;
let U0 be OSAlgebra of S;

let A be OSSubset of U0;

func OSSubSort A -> set equals :: OSALG_2:def 7

{ x where x is Element of SubSort A : x is OrderSortedSet of S } ;

correctness { x where x is Element of SubSort A : x is OrderSortedSet of S } ;

coherence

{ x where x is Element of SubSort A : x is OrderSortedSet of S } is set ;

;

:: deftheorem defines OSSubSort OSALG_2:def 7 :

for S being OrderSortedSign

for U0 being OSAlgebra of S

for A being OSSubset of U0 holds OSSubSort A = { x where x is Element of SubSort A : x is OrderSortedSet of S } ;

for S being OrderSortedSign

for U0 being OSAlgebra of S

for A being OSSubset of U0 holds OSSubSort A = { x where x is Element of SubSort A : x is OrderSortedSet of S } ;

theorem Th16: :: OSALG_2:16

for S1 being OrderSortedSign

for OU0 being OSAlgebra of S1

for A being OSSubset of OU0 holds OSSubSort A c= SubSort A

for OU0 being OSAlgebra of S1

for A being OSSubset of OU0 holds OSSubSort A c= SubSort A

proof end;

theorem Th17: :: OSALG_2:17

for S1 being OrderSortedSign

for OU0 being OSAlgebra of S1

for A being OSSubset of OU0 holds the Sorts of OU0 in OSSubSort A

for OU0 being OSAlgebra of S1

for A being OSSubset of OU0 holds the Sorts of OU0 in OSSubSort A

proof end;

registration

let S1 be OrderSortedSign;

let OU0 be OSAlgebra of S1;

let A be OSSubset of OU0;

coherence

not OSSubSort A is empty by Th17;

end;
let OU0 be OSAlgebra of S1;

let A be OSSubset of OU0;

coherence

not OSSubSort A is empty by Th17;

definition

let S1 be OrderSortedSign;

let OU0 be OSAlgebra of S1;

coherence

{ x where x is Element of SubSort OU0 : x is OrderSortedSet of S1 } is set ;

;

end;
let OU0 be OSAlgebra of S1;

func OSSubSort OU0 -> set equals :: OSALG_2:def 8

{ x where x is Element of SubSort OU0 : x is OrderSortedSet of S1 } ;

correctness { x where x is Element of SubSort OU0 : x is OrderSortedSet of S1 } ;

coherence

{ x where x is Element of SubSort OU0 : x is OrderSortedSet of S1 } is set ;

;

:: deftheorem defines OSSubSort OSALG_2:def 8 :

for S1 being OrderSortedSign

for OU0 being OSAlgebra of S1 holds OSSubSort OU0 = { x where x is Element of SubSort OU0 : x is OrderSortedSet of S1 } ;

for S1 being OrderSortedSign

for OU0 being OSAlgebra of S1 holds OSSubSort OU0 = { x where x is Element of SubSort OU0 : x is OrderSortedSet of S1 } ;

theorem Th18: :: OSALG_2:18

for S1 being OrderSortedSign

for OU0 being OSAlgebra of S1

for A being OSSubset of OU0 holds OSSubSort A c= OSSubSort OU0

for OU0 being OSAlgebra of S1

for A being OSSubset of OU0 holds OSSubSort A c= OSSubSort OU0

proof end;

registration

let S1 be OrderSortedSign;

let OU0 be OSAlgebra of S1;

coherence

not OSSubSort OU0 is empty

end;
let OU0 be OSAlgebra of S1;

coherence

not OSSubSort OU0 is empty

proof end;

:: new-def for order-sorted

definition

let S1 be OrderSortedSign;

let OU0 be OSAlgebra of S1;

let e be Element of OSSubSort OU0;

coherence

e is OSSubset of OU0

end;
let OU0 be OSAlgebra of S1;

let e be Element of OSSubSort OU0;

coherence

e is OSSubset of OU0

proof end;

:: deftheorem defines @ OSALG_2:def 9 :

for S1 being OrderSortedSign

for OU0 being OSAlgebra of S1

for e being Element of OSSubSort OU0 holds @ e = e;

for S1 being OrderSortedSign

for OU0 being OSAlgebra of S1

for e being Element of OSSubSort OU0 holds @ e = e;

:: maybe do another definition of ossort, saying that it contains

:: Elements of subsort which are order-sorted (or ossubsets)

:: Elements of subsort which are order-sorted (or ossubsets)

theorem Th19: :: OSALG_2:19

for S1 being OrderSortedSign

for OU0 being OSAlgebra of S1

for A, B being OSSubset of OU0 holds

( B in OSSubSort A iff ( B is opers_closed & OSConstants OU0 c= B & A c= B ) )

for OU0 being OSAlgebra of S1

for A, B being OSSubset of OU0 holds

( B in OSSubSort A iff ( B is opers_closed & OSConstants OU0 c= B & A c= B ) )

proof end;

theorem Th20: :: OSALG_2:20

for S1 being OrderSortedSign

for OU0 being OSAlgebra of S1

for B being OSSubset of OU0 holds

( B in OSSubSort OU0 iff B is opers_closed )

for OU0 being OSAlgebra of S1

for B being OSSubset of OU0 holds

( B in OSSubSort OU0 iff B is opers_closed )

proof end;

:: slices of members of OSsubsort

definition

let S1 be OrderSortedSign;

let OU0 be OSAlgebra of S1;

let A be OSSubset of OU0;

let s be Element of S1;

ex b_{1} being set st

for x being object holds

( x in b_{1} iff ex B being OSSubset of OU0 st

( B in OSSubSort A & x = B . s ) )

for b_{1}, b_{2} being set st ( for x being object holds

( x in b_{1} iff ex B being OSSubset of OU0 st

( B in OSSubSort A & x = B . s ) ) ) & ( for x being object holds

( x in b_{2} iff ex B being OSSubset of OU0 st

( B in OSSubSort A & x = B . s ) ) ) holds

b_{1} = b_{2}

end;
let OU0 be OSAlgebra of S1;

let A be OSSubset of OU0;

let s be Element of S1;

func OSSubSort (A,s) -> set means :Def10: :: OSALG_2:def 10

for x being object holds

( x in it iff ex B being OSSubset of OU0 st

( B in OSSubSort A & x = B . s ) );

existence for x being object holds

( x in it iff ex B being OSSubset of OU0 st

( B in OSSubSort A & x = B . s ) );

ex b

for x being object holds

( x in b

( B in OSSubSort A & x = B . s ) )

proof end;

uniqueness for b

( x in b

( B in OSSubSort A & x = B . s ) ) ) & ( for x being object holds

( x in b

( B in OSSubSort A & x = B . s ) ) ) holds

b

proof end;

:: deftheorem Def10 defines OSSubSort OSALG_2:def 10 :

for S1 being OrderSortedSign

for OU0 being OSAlgebra of S1

for A being OSSubset of OU0

for s being Element of S1

for b_{5} being set holds

( b_{5} = OSSubSort (A,s) iff for x being object holds

( x in b_{5} iff ex B being OSSubset of OU0 st

( B in OSSubSort A & x = B . s ) ) );

for S1 being OrderSortedSign

for OU0 being OSAlgebra of S1

for A being OSSubset of OU0

for s being Element of S1

for b

( b

( x in b

( B in OSSubSort A & x = B . s ) ) );

theorem Th21: :: OSALG_2:21

for S1 being OrderSortedSign

for OU0 being OSAlgebra of S1

for A being OSSubset of OU0

for s1, s2 being SortSymbol of S1 st s1 <= s2 holds

OSSubSort (A,s2) is_coarser_than OSSubSort (A,s1)

for OU0 being OSAlgebra of S1

for A being OSSubset of OU0

for s1, s2 being SortSymbol of S1 st s1 <= s2 holds

OSSubSort (A,s2) is_coarser_than OSSubSort (A,s1)

proof end;

theorem Th22: :: OSALG_2:22

for S1 being OrderSortedSign

for OU0 being OSAlgebra of S1

for A being OSSubset of OU0

for s being SortSymbol of S1 holds OSSubSort (A,s) c= SubSort (A,s)

for OU0 being OSAlgebra of S1

for A being OSSubset of OU0

for s being SortSymbol of S1 holds OSSubSort (A,s) c= SubSort (A,s)

proof end;

theorem Th23: :: OSALG_2:23

for S1 being OrderSortedSign

for OU0 being OSAlgebra of S1

for A being OSSubset of OU0

for s being SortSymbol of S1 holds the Sorts of OU0 . s in OSSubSort (A,s)

for OU0 being OSAlgebra of S1

for A being OSSubset of OU0

for s being SortSymbol of S1 holds the Sorts of OU0 . s in OSSubSort (A,s)

proof end;

registration

let S1 be OrderSortedSign;

let OU0 be OSAlgebra of S1;

let A be OSSubset of OU0;

let s be SortSymbol of S1;

coherence

not OSSubSort (A,s) is empty by Th23;

end;
let OU0 be OSAlgebra of S1;

let A be OSSubset of OU0;

let s be SortSymbol of S1;

coherence

not OSSubSort (A,s) is empty by Th23;

definition

let S1 be OrderSortedSign;

let OU0 be OSAlgebra of S1;

let A be OSSubset of OU0;

ex b_{1} being OSSubset of OU0 st

for s being SortSymbol of S1 holds b_{1} . s = meet (OSSubSort (A,s))

for b_{1}, b_{2} being OSSubset of OU0 st ( for s being SortSymbol of S1 holds b_{1} . s = meet (OSSubSort (A,s)) ) & ( for s being SortSymbol of S1 holds b_{2} . s = meet (OSSubSort (A,s)) ) holds

b_{1} = b_{2}

end;
let OU0 be OSAlgebra of S1;

let A be OSSubset of OU0;

func OSMSubSort A -> OSSubset of OU0 means :Def11: :: OSALG_2:def 11

for s being SortSymbol of S1 holds it . s = meet (OSSubSort (A,s));

existence for s being SortSymbol of S1 holds it . s = meet (OSSubSort (A,s));

ex b

for s being SortSymbol of S1 holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def11 defines OSMSubSort OSALG_2:def 11 :

for S1 being OrderSortedSign

for OU0 being OSAlgebra of S1

for A, b_{4} being OSSubset of OU0 holds

( b_{4} = OSMSubSort A iff for s being SortSymbol of S1 holds b_{4} . s = meet (OSSubSort (A,s)) );

for S1 being OrderSortedSign

for OU0 being OSAlgebra of S1

for A, b

( b

registration

let S1 be OrderSortedSign;

let OU0 be OSAlgebra of S1;

ex b_{1} being OSSubset of OU0 st b_{1} is opers_closed

end;
let OU0 be OSAlgebra of S1;

cluster non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) opers_closed for OSSubset of OU0;

existence ex b

proof end;

theorem Th24: :: OSALG_2:24

for S1 being OrderSortedSign

for OU0 being OSAlgebra of S1

for A being OSSubset of OU0 holds (OSConstants OU0) (\/) A c= OSMSubSort A

for OU0 being OSAlgebra of S1

for A being OSSubset of OU0 holds (OSConstants OU0) (\/) A c= OSMSubSort A

proof end;

theorem :: OSALG_2:25

for S1 being OrderSortedSign

for OU0 being OSAlgebra of S1

for A being OSSubset of OU0 st (OSConstants OU0) (\/) A is V8() holds

OSMSubSort A is V8()

for OU0 being OSAlgebra of S1

for A being OSSubset of OU0 st (OSConstants OU0) (\/) A is V8() holds

OSMSubSort A is V8()

proof end;

theorem Th26: :: OSALG_2:26

for S1 being OrderSortedSign

for OU0 being OSAlgebra of S1

for o being OperSymbol of S1

for A, B being OSSubset of OU0 st B in OSSubSort A holds

(((OSMSubSort A) #) * the Arity of S1) . o c= ((B #) * the Arity of S1) . o

for OU0 being OSAlgebra of S1

for o being OperSymbol of S1

for A, B being OSSubset of OU0 st B in OSSubSort A holds

(((OSMSubSort A) #) * the Arity of S1) . o c= ((B #) * the Arity of S1) . o

proof end;

theorem Th27: :: OSALG_2:27

for S1 being OrderSortedSign

for OU0 being OSAlgebra of S1

for o being OperSymbol of S1

for A, B being OSSubset of OU0 st B in OSSubSort A holds

rng ((Den (o,OU0)) | ((((OSMSubSort A) #) * the Arity of S1) . o)) c= (B * the ResultSort of S1) . o

for OU0 being OSAlgebra of S1

for o being OperSymbol of S1

for A, B being OSSubset of OU0 st B in OSSubSort A holds

rng ((Den (o,OU0)) | ((((OSMSubSort A) #) * the Arity of S1) . o)) c= (B * the ResultSort of S1) . o

proof end;

theorem Th28: :: OSALG_2:28

for S1 being OrderSortedSign

for OU0 being OSAlgebra of S1

for o being OperSymbol of S1

for A being OSSubset of OU0 holds rng ((Den (o,OU0)) | ((((OSMSubSort A) #) * the Arity of S1) . o)) c= ((OSMSubSort A) * the ResultSort of S1) . o

for OU0 being OSAlgebra of S1

for o being OperSymbol of S1

for A being OSSubset of OU0 holds rng ((Den (o,OU0)) | ((((OSMSubSort A) #) * the Arity of S1) . o)) c= ((OSMSubSort A) * the ResultSort of S1) . o

proof end;

theorem Th29: :: OSALG_2:29

for S1 being OrderSortedSign

for OU0 being OSAlgebra of S1

for A being OSSubset of OU0 holds

( OSMSubSort A is opers_closed & A c= OSMSubSort A )

for OU0 being OSAlgebra of S1

for A being OSSubset of OU0 holds

( OSMSubSort A is opers_closed & A c= OSMSubSort A )

proof end;

registration

let S1 be OrderSortedSign;

let OU0 be OSAlgebra of S1;

let A be OSSubset of OU0;

coherence

OSMSubSort A is opers_closed by Th29;

end;
let OU0 be OSAlgebra of S1;

let A be OSSubset of OU0;

coherence

OSMSubSort A is opers_closed by Th29;

registration

let S1 be OrderSortedSign;

let OU0 be OSAlgebra of S1;

let A be opers_closed OSSubset of OU0;

coherence

OU0 | A is order-sorted

end;
let OU0 be OSAlgebra of S1;

let A be opers_closed OSSubset of OU0;

coherence

OU0 | A is order-sorted

proof end;

registration

let S1 be OrderSortedSign;

let OU0 be OSAlgebra of S1;

let OU1, OU2 be OSSubAlgebra of OU0;

coherence

OU1 /\ OU2 is order-sorted

end;
let OU0 be OSAlgebra of S1;

let OU1, OU2 be OSSubAlgebra of OU0;

coherence

OU1 /\ OU2 is order-sorted

proof end;

:: generally, GenOSAlg can differ from GenMSAlg, example should be given

definition

let S1 be OrderSortedSign;

let OU0 be OSAlgebra of S1;

let A be OSSubset of OU0;

ex b_{1} being strict OSSubAlgebra of OU0 st

( A is OSSubset of b_{1} & ( for OU1 being OSSubAlgebra of OU0 st A is OSSubset of OU1 holds

b_{1} is OSSubAlgebra of OU1 ) )

for b_{1}, b_{2} being strict OSSubAlgebra of OU0 st A is OSSubset of b_{1} & ( for OU1 being OSSubAlgebra of OU0 st A is OSSubset of OU1 holds

b_{1} is OSSubAlgebra of OU1 ) & A is OSSubset of b_{2} & ( for OU1 being OSSubAlgebra of OU0 st A is OSSubset of OU1 holds

b_{2} is OSSubAlgebra of OU1 ) holds

b_{1} = b_{2}

end;
let OU0 be OSAlgebra of S1;

let A be OSSubset of OU0;

func GenOSAlg A -> strict OSSubAlgebra of OU0 means :Def12: :: OSALG_2:def 12

( A is OSSubset of it & ( for OU1 being OSSubAlgebra of OU0 st A is OSSubset of OU1 holds

it is OSSubAlgebra of OU1 ) );

existence ( A is OSSubset of it & ( for OU1 being OSSubAlgebra of OU0 st A is OSSubset of OU1 holds

it is OSSubAlgebra of OU1 ) );

ex b

( A is OSSubset of b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def12 defines GenOSAlg OSALG_2:def 12 :

for S1 being OrderSortedSign

for OU0 being OSAlgebra of S1

for A being OSSubset of OU0

for b_{4} being strict OSSubAlgebra of OU0 holds

( b_{4} = GenOSAlg A iff ( A is OSSubset of b_{4} & ( for OU1 being OSSubAlgebra of OU0 st A is OSSubset of OU1 holds

b_{4} is OSSubAlgebra of OU1 ) ) );

for S1 being OrderSortedSign

for OU0 being OSAlgebra of S1

for A being OSSubset of OU0

for b

( b

b

:: this should rather be a definition, but I want to keep

:: compatibility of the definition with MSUALG_2

:: compatibility of the definition with MSUALG_2

theorem Th30: :: OSALG_2:30

for S1 being OrderSortedSign

for OU0 being OSAlgebra of S1

for A being OSSubset of OU0 holds

( GenOSAlg A = OU0 | (OSMSubSort A) & the Sorts of (GenOSAlg A) = OSMSubSort A )

for OU0 being OSAlgebra of S1

for A being OSSubset of OU0 holds

( GenOSAlg A = OU0 | (OSMSubSort A) & the Sorts of (GenOSAlg A) = OSMSubSort A )

proof end;

:: this could simplify some proofs in MSUALG_2, I need it anyway

theorem Th31: :: OSALG_2:31

for S being non empty non void ManySortedSign

for U0 being MSAlgebra over S

for A being MSSubset of U0 holds

( GenMSAlg A = U0 | (MSSubSort A) & the Sorts of (GenMSAlg A) = MSSubSort A )

for U0 being MSAlgebra over S

for A being MSSubset of U0 holds

( GenMSAlg A = U0 | (MSSubSort A) & the Sorts of (GenMSAlg A) = MSSubSort A )

proof end;

theorem Th32: :: OSALG_2:32

for S1 being OrderSortedSign

for OU0 being OSAlgebra of S1

for A being OSSubset of OU0 holds the Sorts of (GenMSAlg A) c= the Sorts of (GenOSAlg A)

for OU0 being OSAlgebra of S1

for A being OSSubset of OU0 holds the Sorts of (GenMSAlg A) c= the Sorts of (GenOSAlg A)

proof end;

theorem :: OSALG_2:33

for S1 being OrderSortedSign

for OU0 being OSAlgebra of S1

for A being OSSubset of OU0 holds GenMSAlg A is MSSubAlgebra of GenOSAlg A by Th32, MSUALG_2:8;

for OU0 being OSAlgebra of S1

for A being OSSubset of OU0 holds GenMSAlg A is MSSubAlgebra of GenOSAlg A by Th32, MSUALG_2:8;

theorem Th34: :: OSALG_2:34

for S1 being OrderSortedSign

for OU0 being strict OSAlgebra of S1

for B being OSSubset of OU0 st B = the Sorts of OU0 holds

GenOSAlg B = OU0

for OU0 being strict OSAlgebra of S1

for B being OSSubset of OU0 st B = the Sorts of OU0 holds

GenOSAlg B = OU0

proof end;

theorem Th35: :: OSALG_2:35

for S1 being OrderSortedSign

for OU0 being OSAlgebra of S1

for OU1 being strict OSSubAlgebra of OU0

for B being OSSubset of OU0 st B = the Sorts of OU1 holds

GenOSAlg B = OU1

for OU0 being OSAlgebra of S1

for OU1 being strict OSSubAlgebra of OU0

for B being OSSubset of OU0 st B = the Sorts of OU1 holds

GenOSAlg B = OU1

proof end;

theorem Th36: :: OSALG_2:36

for S1 being OrderSortedSign

for U0 being non-empty OSAlgebra of S1

for U1 being OSSubAlgebra of U0 holds (GenOSAlg (OSConstants U0)) /\ U1 = GenOSAlg (OSConstants U0)

for U0 being non-empty OSAlgebra of S1

for U1 being OSSubAlgebra of U0 holds (GenOSAlg (OSConstants U0)) /\ U1 = GenOSAlg (OSConstants U0)

proof end;

definition

let S1 be OrderSortedSign;

let U0 be non-empty OSAlgebra of S1;

let U1, U2 be OSSubAlgebra of U0;

ex b_{1} being strict OSSubAlgebra of U0 st

for A being OSSubset of U0 st A = the Sorts of U1 (\/) the Sorts of U2 holds

b_{1} = GenOSAlg A

for b_{1}, b_{2} being strict OSSubAlgebra of U0 st ( for A being OSSubset of U0 st A = the Sorts of U1 (\/) the Sorts of U2 holds

b_{1} = GenOSAlg A ) & ( for A being OSSubset of U0 st A = the Sorts of U1 (\/) the Sorts of U2 holds

b_{2} = GenOSAlg A ) holds

b_{1} = b_{2}

end;
let U0 be non-empty OSAlgebra of S1;

let U1, U2 be OSSubAlgebra of U0;

func U1 "\/"_os U2 -> strict OSSubAlgebra of U0 means :Def13: :: OSALG_2:def 13

for A being OSSubset of U0 st A = the Sorts of U1 (\/) the Sorts of U2 holds

it = GenOSAlg A;

existence for A being OSSubset of U0 st A = the Sorts of U1 (\/) the Sorts of U2 holds

it = GenOSAlg A;

ex b

for A being OSSubset of U0 st A = the Sorts of U1 (\/) the Sorts of U2 holds

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def13 defines "\/"_os OSALG_2:def 13 :

for S1 being OrderSortedSign

for U0 being non-empty OSAlgebra of S1

for U1, U2 being OSSubAlgebra of U0

for b_{5} being strict OSSubAlgebra of U0 holds

( b_{5} = U1 "\/"_os U2 iff for A being OSSubset of U0 st A = the Sorts of U1 (\/) the Sorts of U2 holds

b_{5} = GenOSAlg A );

for S1 being OrderSortedSign

for U0 being non-empty OSAlgebra of S1

for U1, U2 being OSSubAlgebra of U0

for b

( b

b

theorem Th37: :: OSALG_2:37

for S1 being OrderSortedSign

for U0 being non-empty OSAlgebra of S1

for U1 being OSSubAlgebra of U0

for A, B being OSSubset of U0 st B = A (\/) the Sorts of U1 holds

(GenOSAlg A) "\/"_os U1 = GenOSAlg B

for U0 being non-empty OSAlgebra of S1

for U1 being OSSubAlgebra of U0

for A, B being OSSubset of U0 st B = A (\/) the Sorts of U1 holds

(GenOSAlg A) "\/"_os U1 = GenOSAlg B

proof end;

theorem Th38: :: OSALG_2:38

for S1 being OrderSortedSign

for U0 being non-empty OSAlgebra of S1

for U1 being OSSubAlgebra of U0

for B being OSSubset of U0 st B = the Sorts of U0 holds

(GenOSAlg B) "\/"_os U1 = GenOSAlg B

for U0 being non-empty OSAlgebra of S1

for U1 being OSSubAlgebra of U0

for B being OSSubset of U0 st B = the Sorts of U0 holds

(GenOSAlg B) "\/"_os U1 = GenOSAlg B

proof end;

theorem Th39: :: OSALG_2:39

for S1 being OrderSortedSign

for U0 being non-empty OSAlgebra of S1

for U1, U2 being OSSubAlgebra of U0 holds U1 "\/"_os U2 = U2 "\/"_os U1

for U0 being non-empty OSAlgebra of S1

for U1, U2 being OSSubAlgebra of U0 holds U1 "\/"_os U2 = U2 "\/"_os U1

proof end;

theorem Th40: :: OSALG_2:40

for S1 being OrderSortedSign

for U0 being non-empty OSAlgebra of S1

for U1, U2 being strict OSSubAlgebra of U0 holds U1 /\ (U1 "\/"_os U2) = U1

for U0 being non-empty OSAlgebra of S1

for U1, U2 being strict OSSubAlgebra of U0 holds U1 /\ (U1 "\/"_os U2) = U1

proof end;

theorem Th41: :: OSALG_2:41

for S1 being OrderSortedSign

for U0 being non-empty OSAlgebra of S1

for U1, U2 being strict OSSubAlgebra of U0 holds (U1 /\ U2) "\/"_os U2 = U2

for U0 being non-empty OSAlgebra of S1

for U1, U2 being strict OSSubAlgebra of U0 holds (U1 /\ U2) "\/"_os U2 = U2

proof end;

:: ossub, ossubalgebra

definition

let S1 be OrderSortedSign;

let OU0 be OSAlgebra of S1;

ex b_{1} being set st

for x being object holds

( x in b_{1} iff x is strict OSSubAlgebra of OU0 )

for b_{1}, b_{2} being set st ( for x being object holds

( x in b_{1} iff x is strict OSSubAlgebra of OU0 ) ) & ( for x being object holds

( x in b_{2} iff x is strict OSSubAlgebra of OU0 ) ) holds

b_{1} = b_{2}

end;
let OU0 be OSAlgebra of S1;

func OSSub OU0 -> set means :Def14: :: OSALG_2:def 14

for x being object holds

( x in it iff x is strict OSSubAlgebra of OU0 );

existence for x being object holds

( x in it iff x is strict OSSubAlgebra of OU0 );

ex b

for x being object holds

( x in b

proof end;

uniqueness for b

( x in b

( x in b

b

proof end;

:: deftheorem Def14 defines OSSub OSALG_2:def 14 :

for S1 being OrderSortedSign

for OU0 being OSAlgebra of S1

for b_{3} being set holds

( b_{3} = OSSub OU0 iff for x being object holds

( x in b_{3} iff x is strict OSSubAlgebra of OU0 ) );

for S1 being OrderSortedSign

for OU0 being OSAlgebra of S1

for b

( b

( x in b

registration
end;

definition

let S1 be OrderSortedSign;

let OU0 be OSAlgebra of S1;

:: original: OSSub

redefine func OSSub OU0 -> Subset of (MSSub OU0);

coherence

OSSub OU0 is Subset of (MSSub OU0) by Th42;

end;
let OU0 be OSAlgebra of S1;

:: original: OSSub

redefine func OSSub OU0 -> Subset of (MSSub OU0);

coherence

OSSub OU0 is Subset of (MSSub OU0) by Th42;

:: maybe show that e.g. for TrivialOSA(S,z,z1), OSSub(U0) is

:: proper subset of MSSub(U0), to have some counterexamples

:: proper subset of MSSub(U0), to have some counterexamples

definition

let S1 be OrderSortedSign;

let U0 be non-empty OSAlgebra of S1;

ex b_{1} being BinOp of (OSSub U0) st

for x, y being Element of OSSub U0

for U1, U2 being strict OSSubAlgebra of U0 st x = U1 & y = U2 holds

b_{1} . (x,y) = U1 "\/"_os U2

for b_{1}, b_{2} being BinOp of (OSSub U0) st ( for x, y being Element of OSSub U0

for U1, U2 being strict OSSubAlgebra of U0 st x = U1 & y = U2 holds

b_{1} . (x,y) = U1 "\/"_os U2 ) & ( for x, y being Element of OSSub U0

for U1, U2 being strict OSSubAlgebra of U0 st x = U1 & y = U2 holds

b_{2} . (x,y) = U1 "\/"_os U2 ) holds

b_{1} = b_{2}

end;
let U0 be non-empty OSAlgebra of S1;

func OSAlg_join U0 -> BinOp of (OSSub U0) means :Def15: :: OSALG_2:def 15

for x, y being Element of OSSub U0

for U1, U2 being strict OSSubAlgebra of U0 st x = U1 & y = U2 holds

it . (x,y) = U1 "\/"_os U2;

existence for x, y being Element of OSSub U0

for U1, U2 being strict OSSubAlgebra of U0 st x = U1 & y = U2 holds

it . (x,y) = U1 "\/"_os U2;

ex b

for x, y being Element of OSSub U0

for U1, U2 being strict OSSubAlgebra of U0 st x = U1 & y = U2 holds

b

proof end;

uniqueness for b

for U1, U2 being strict OSSubAlgebra of U0 st x = U1 & y = U2 holds

b

for U1, U2 being strict OSSubAlgebra of U0 st x = U1 & y = U2 holds

b

b

proof end;

:: deftheorem Def15 defines OSAlg_join OSALG_2:def 15 :

for S1 being OrderSortedSign

for U0 being non-empty OSAlgebra of S1

for b_{3} being BinOp of (OSSub U0) holds

( b_{3} = OSAlg_join U0 iff for x, y being Element of OSSub U0

for U1, U2 being strict OSSubAlgebra of U0 st x = U1 & y = U2 holds

b_{3} . (x,y) = U1 "\/"_os U2 );

for S1 being OrderSortedSign

for U0 being non-empty OSAlgebra of S1

for b

( b

for U1, U2 being strict OSSubAlgebra of U0 st x = U1 & y = U2 holds

b

definition

let S1 be OrderSortedSign;

let U0 be non-empty OSAlgebra of S1;

ex b_{1} being BinOp of (OSSub U0) st

for x, y being Element of OSSub U0

for U1, U2 being strict OSSubAlgebra of U0 st x = U1 & y = U2 holds

b_{1} . (x,y) = U1 /\ U2

for b_{1}, b_{2} being BinOp of (OSSub U0) st ( for x, y being Element of OSSub U0

for U1, U2 being strict OSSubAlgebra of U0 st x = U1 & y = U2 holds

b_{1} . (x,y) = U1 /\ U2 ) & ( for x, y being Element of OSSub U0

for U1, U2 being strict OSSubAlgebra of U0 st x = U1 & y = U2 holds

b_{2} . (x,y) = U1 /\ U2 ) holds

b_{1} = b_{2}

end;
let U0 be non-empty OSAlgebra of S1;

func OSAlg_meet U0 -> BinOp of (OSSub U0) means :Def16: :: OSALG_2:def 16

for x, y being Element of OSSub U0

for U1, U2 being strict OSSubAlgebra of U0 st x = U1 & y = U2 holds

it . (x,y) = U1 /\ U2;

existence for x, y being Element of OSSub U0

for U1, U2 being strict OSSubAlgebra of U0 st x = U1 & y = U2 holds

it . (x,y) = U1 /\ U2;

ex b

for x, y being Element of OSSub U0

for U1, U2 being strict OSSubAlgebra of U0 st x = U1 & y = U2 holds

b

proof end;

uniqueness for b

for U1, U2 being strict OSSubAlgebra of U0 st x = U1 & y = U2 holds

b

for U1, U2 being strict OSSubAlgebra of U0 st x = U1 & y = U2 holds

b

b

proof end;

:: deftheorem Def16 defines OSAlg_meet OSALG_2:def 16 :

for S1 being OrderSortedSign

for U0 being non-empty OSAlgebra of S1

for b_{3} being BinOp of (OSSub U0) holds

( b_{3} = OSAlg_meet U0 iff for x, y being Element of OSSub U0

for U1, U2 being strict OSSubAlgebra of U0 st x = U1 & y = U2 holds

b_{3} . (x,y) = U1 /\ U2 );

for S1 being OrderSortedSign

for U0 being non-empty OSAlgebra of S1

for b

( b

for U1, U2 being strict OSSubAlgebra of U0 st x = U1 & y = U2 holds

b

theorem Th43: :: OSALG_2:43

for S1 being OrderSortedSign

for U0 being non-empty OSAlgebra of S1

for x, y being Element of OSSub U0 holds (OSAlg_meet U0) . (x,y) = (MSAlg_meet U0) . (x,y)

for U0 being non-empty OSAlgebra of S1

for x, y being Element of OSSub U0 holds (OSAlg_meet U0) . (x,y) = (MSAlg_meet U0) . (x,y)

proof end;

theorem Th44: :: OSALG_2:44

for S1 being OrderSortedSign

for U0 being non-empty OSAlgebra of S1 holds OSAlg_join U0 is commutative

for U0 being non-empty OSAlgebra of S1 holds OSAlg_join U0 is commutative

proof end;

theorem Th45: :: OSALG_2:45

for S1 being OrderSortedSign

for U0 being non-empty OSAlgebra of S1 holds OSAlg_join U0 is associative

for U0 being non-empty OSAlgebra of S1 holds OSAlg_join U0 is associative

proof end;

theorem Th46: :: OSALG_2:46

for S1 being OrderSortedSign

for U0 being non-empty OSAlgebra of S1 holds OSAlg_meet U0 is commutative

for U0 being non-empty OSAlgebra of S1 holds OSAlg_meet U0 is commutative

proof end;

theorem Th47: :: OSALG_2:47

for S1 being OrderSortedSign

for U0 being non-empty OSAlgebra of S1 holds OSAlg_meet U0 is associative

for U0 being non-empty OSAlgebra of S1 holds OSAlg_meet U0 is associative

proof end;

definition

let S1 be OrderSortedSign;

let U0 be non-empty OSAlgebra of S1;

LattStr(# (OSSub U0),(OSAlg_join U0),(OSAlg_meet U0) #) is strict Lattice

end;
let U0 be non-empty OSAlgebra of S1;

func OSSubAlLattice U0 -> strict Lattice equals :: OSALG_2:def 17

LattStr(# (OSSub U0),(OSAlg_join U0),(OSAlg_meet U0) #);

coherence LattStr(# (OSSub U0),(OSAlg_join U0),(OSAlg_meet U0) #);

LattStr(# (OSSub U0),(OSAlg_join U0),(OSAlg_meet U0) #) is strict Lattice

proof end;

:: deftheorem defines OSSubAlLattice OSALG_2:def 17 :

for S1 being OrderSortedSign

for U0 being non-empty OSAlgebra of S1 holds OSSubAlLattice U0 = LattStr(# (OSSub U0),(OSAlg_join U0),(OSAlg_meet U0) #);

for S1 being OrderSortedSign

for U0 being non-empty OSAlgebra of S1 holds OSSubAlLattice U0 = LattStr(# (OSSub U0),(OSAlg_join U0),(OSAlg_meet U0) #);

theorem Th48: :: OSALG_2:48

for S1 being OrderSortedSign

for U0 being non-empty OSAlgebra of S1 holds OSSubAlLattice U0 is bounded

for U0 being non-empty OSAlgebra of S1 holds OSSubAlLattice U0 is bounded

proof end;

registration

let S1 be OrderSortedSign;

let U0 be non-empty OSAlgebra of S1;

coherence

OSSubAlLattice U0 is bounded by Th48;

end;
let U0 be non-empty OSAlgebra of S1;

coherence

OSSubAlLattice U0 is bounded by Th48;

theorem :: OSALG_2:49

for S1 being OrderSortedSign

for U0 being non-empty OSAlgebra of S1 holds Bottom (OSSubAlLattice U0) = GenOSAlg (OSConstants U0)

for U0 being non-empty OSAlgebra of S1 holds Bottom (OSSubAlLattice U0) = GenOSAlg (OSConstants U0)

proof end;

theorem Th50: :: OSALG_2:50

for S1 being OrderSortedSign

for U0 being non-empty OSAlgebra of S1

for B being OSSubset of U0 st B = the Sorts of U0 holds

Top (OSSubAlLattice U0) = GenOSAlg B

for U0 being non-empty OSAlgebra of S1

for B being OSSubset of U0 st B = the Sorts of U0 holds

Top (OSSubAlLattice U0) = GenOSAlg B

proof end;

theorem :: OSALG_2:51

for S1 being OrderSortedSign

for U0 being strict non-empty OSAlgebra of S1 holds Top (OSSubAlLattice U0) = U0

for U0 being strict non-empty OSAlgebra of S1 holds Top (OSSubAlLattice U0) = U0

proof end;