:: Subalgebras of a Order Sorted Algebra. {L}attice of Subalgebras
:: by Josef Urban
::
:: Received September 19, 2002
:: Copyright (c) 2002-2012 Association of Mizar Users


begin

:: 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
proofend;

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
proofend;

:: new and bad
definition
let R be non empty Poset;
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
 ex b1 being ManySortedSubset of M st b1 is OrderSortedSet of R
proofend;
end;

:: deftheorem Def1 defines OrderSortedSubset OSALG_2:def_1_:_
 for R being non empty Poset
for M being OrderSortedSet of R
for b3 being ManySortedSubset of M holds
( b3 is OrderSortedSubset of M iff b3 is OrderSortedSet of R );

registration
let R be non empty Poset;
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 b1 being OrderSortedSubset of M holds b1 is V8()
proofend;
end;

begin

::
:: Constants of an Order Sorted Algebra.
::
definition
let S be OrderSortedSign;
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
 ex b1 being ManySortedSubset of the Sorts of U0 st b1 is OrderSortedSet of S
proofend;
end;

:: deftheorem Def2 defines OSSubset OSALG_2:def_2_:_
 for S being OrderSortedSign
for U0 being OSAlgebra of S
for b3 being ManySortedSubset of the Sorts of U0 holds
( b3 is OSSubset of U0 iff b3 is OrderSortedSet of S );

:: very strange, the cluster in OSALG_1 should take care of this one
registration
let S be OrderSortedSign;
cluster strict non-empty order-sorted monotone for MSAlgebra over S;
existence
 ex b1 being OSAlgebra of S st
( b1 is monotone & b1 is strict & b1 is non-empty )
proofend;
end;

registration
let S be OrderSortedSign;
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 b1 being OSSubset of U0 holds b1 is V8()
proofend;
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
proofend;

registration
cluster non empty non void V52() all-with_const_op V99() V100() V101() strict order-sorted discernable for OverloadedRSSign ;
existence
 ex b1 being OrderSortedSign st
( b1 is all-with_const_op & b1 is strict )
proofend;
end;

begin

::
:: 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
proofend;

registration
let S be OrderSortedSign;
let U0 be OSAlgebra of S;
cluster order-sorted for MSSubAlgebra of U0;
existence
 ex b1 being MSSubAlgebra of U0 st b1 is order-sorted
proofend;
end;

definition
let S be OrderSortedSign;
let U0 be OSAlgebra of S;
mode OSSubAlgebra of U0 is order-sorted MSSubAlgebra of U0;
end;

registration
let S be OrderSortedSign;
let U0 be OSAlgebra of S;
cluster strict order-sorted for MSSubAlgebra of U0;
existence
 ex b1 being OSSubAlgebra of U0 st b1 is strict
proofend;
end;

registration
let S be OrderSortedSign;
let U0 be non-empty OSAlgebra of S;
cluster strict non-empty order-sorted for MSSubAlgebra of U0;
existence
 ex b1 being OSSubAlgebra of U0 st
( b1 is non-empty & b1 is strict )
proofend;
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) ) ) ) )
proofend;

definition
let S1 be OrderSortedSign;
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  }  is Subset of ( the Sorts of OU0 . s)
proofend;
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  }  ;

:: maybe
:: 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)
proofend;

definition
let S1 be OrderSortedSign;
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
 ex b1 being OrderSortedSet of S1 st
for s being SortSymbol of S1 holds b1 . s = union  {  (M . s1) where s1 is SortSymbol of S1 : s1 <= s  }
proofend;
uniqueness
 for b1, b2 being OrderSortedSet of S1 st ( for s being SortSymbol of S1 holds b1 . s = union  {  (M . s1) where s1 is SortSymbol of S1 : s1 <= s  }  ) &amp; ( for s being SortSymbol of S1 holds b2 . s = union  {  (M . s1) where s1 is SortSymbol of S1 : s1 <= s  }  ) holds
b1 = b2
proofend;
end;

:: deftheorem Def4 defines OSCl OSALG_2:def_4_:_
 for S1 being OrderSortedSign
for M being ManySortedSet of the carrier of S1
for b3 being OrderSortedSet of S1 holds
( b3 = OSCl M iff for s being SortSymbol of S1 holds b3 . s = union  {  (M . s1) where s1 is SortSymbol of S1 : s1 <= s  }  );

theorem Th7: :: OSALG_2:7
for S1 being OrderSortedSign
for M being ManySortedSet of the carrier of S1 holds M c= OSCl M
proofend;

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
proofend;

theorem :: OSALG_2:9
for S being OrderSortedSign
for X being OrderSortedSet of S holds OSCl X = X
proofend;

:: following should be rewritten to use OSCl Constants(OU0) instead;
:: maybe later
definition
let S1 be OrderSortedSign;
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
 ex b1 being OSSubset of OU0 st
for s being SortSymbol of S1 holds b1 . s = OSConstants (OU0,s)
proofend;
uniqueness
 for b1, b2 being OSSubset of OU0 st ( for s being SortSymbol of S1 holds b1 . s = OSConstants (OU0,s) ) &amp; ( for s being SortSymbol of S1 holds b2 . s = OSConstants (OU0,s) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def5 defines OSConstants OSALG_2:def_5_:_
 for S1 being OrderSortedSign
for OU0 being OSAlgebra of S1
for b3 being OSSubset of OU0 holds
( b3 = OSConstants OU0 iff for s being SortSymbol of S1 holds b3 . s = OSConstants (OU0,s) );

theorem Th10: :: OSALG_2:10
for S1 being OrderSortedSign
for OU0 being OSAlgebra of S1 holds Constants OU0 c= OSConstants OU0
proofend;

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
proofend;

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)
proofend;

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
proofend;

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
proofend;

begin

::
:: 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) )
proofend;

:: Fraenkel should be improved, to allow more than just Element type
definition
let R be non empty Poset;
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
 ex b1 being set st
for x being set holds
( x in b1 iff x is OrderSortedSubset of M )
proofend;
uniqueness
 for b1, b2 being set st ( for x being set holds
( x in b1 iff x is OrderSortedSubset of M ) ) &amp; ( for x being set holds
( x in b2 iff x is OrderSortedSubset of M ) ) holds
b1 = b2
proofend;
end;

:: deftheorem  defines OSbool OSALG_2:def_6_:_
 for R being non empty Poset
for M being OrderSortedSet of R
for b3 being set holds
( b3 = OSbool M iff for x being set holds
( x in b3 iff x is OrderSortedSubset of M ) );

definition
let S be OrderSortedSign;
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
coherence
{  x where x is Element of SubSort A : x is OrderSortedSet of S  }  is set ;
;
end;

:: 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  }  ;

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
proofend;

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
proofend;

registration
let S1 be OrderSortedSign;
let OU0 be OSAlgebra of S1;
let A be OSSubset of OU0;
cluster OSSubSort A ->  non empty ;
coherence
 not OSSubSort A is empty by Th17;
end;

definition
let S1 be OrderSortedSign;
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
coherence
{  x where x is Element of SubSort OU0 : x is OrderSortedSet of S1  }  is set ;
;
end;

:: 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  }  ;

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
proofend;

registration
let S1 be OrderSortedSign;
let OU0 be OSAlgebra of S1;
cluster OSSubSort OU0 ->  non empty ;
coherence
 not OSSubSort OU0 is empty
proofend;
end;

:: new-def for order-sorted
definition
let S1 be OrderSortedSign;
let OU0 be OSAlgebra of S1;
let e be Element of OSSubSort OU0;
func @ e ->  OSSubset of OU0 equals :: OSALG_2:def 9
e;
coherence
 e is OSSubset of OU0
proofend;
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;

:: maybe do another definition of ossort, saying that it contains
:: 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 &amp; OSConstants OU0 c= B &amp; A c= B ) )
proofend;

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 )
proofend;

:: 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;
func OSSubSort (A,s) ->  set  means :Def10: :: OSALG_2:def 10
 for x being set holds
( x in it iff ex B being OSSubset of OU0 st
( B in OSSubSort A &amp; x = B . s ) );
existence
 ex b1 being set st
for x being set holds
( x in b1 iff ex B being OSSubset of OU0 st
( B in OSSubSort A &amp; x = B . s ) )
proofend;
uniqueness
 for b1, b2 being set st ( for x being set holds
( x in b1 iff ex B being OSSubset of OU0 st
( B in OSSubSort A &amp; x = B . s ) ) ) &amp; ( for x being set holds
( x in b2 iff ex B being OSSubset of OU0 st
( B in OSSubSort A &amp; x = B . s ) ) ) holds
b1 = b2
proofend;
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 b5 being set holds
( b5 = OSSubSort (A,s) iff for x being set holds
( x in b5 iff ex B being OSSubset of OU0 st
( B in OSSubSort A &amp; 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)
proofend;

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)
proofend;

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)
proofend;

registration
let S1 be OrderSortedSign;
let OU0 be OSAlgebra of S1;
let A be OSSubset of OU0;
let s be SortSymbol of S1;
cluster OSSubSort (A,s) ->  non empty ;
coherence
 not OSSubSort (A,s) is empty by Th23;
end;

definition
let S1 be OrderSortedSign;
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
 ex b1 being OSSubset of OU0 st
for s being SortSymbol of S1 holds b1 . s = meet (OSSubSort (A,s))
proofend;
uniqueness
 for b1, b2 being OSSubset of OU0 st ( for s being SortSymbol of S1 holds b1 . s = meet (OSSubSort (A,s)) ) &amp; ( for s being SortSymbol of S1 holds b2 . s = meet (OSSubSort (A,s)) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def11 defines OSMSubSort OSALG_2:def_11_:_
 for S1 being OrderSortedSign
for OU0 being OSAlgebra of S1
for A, b4 being OSSubset of OU0 holds
( b4 = OSMSubSort A iff for s being SortSymbol of S1 holds b4 . s = meet (OSSubSort (A,s)) );

registration
let S1 be OrderSortedSign;
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 b1 being OSSubset of OU0 st b1 is opers_closed
proofend;
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
proofend;

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()
proofend;

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
proofend;

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
proofend;

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
proofend;

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 &amp; A c= OSMSubSort A )
proofend;

registration
let S1 be OrderSortedSign;
let OU0 be OSAlgebra of S1;
let A be OSSubset of OU0;
cluster OSMSubSort A ->  opers_closed ;
coherence
 OSMSubSort A is opers_closed by Th29;
end;

begin

registration
let S1 be OrderSortedSign;
let OU0 be OSAlgebra of S1;
let A be opers_closed OSSubset of OU0;
clusterOU0 | A ->  order-sorted ;
coherence
 OU0 | A is order-sorted
proofend;
end;

registration
let S1 be OrderSortedSign;
let OU0 be OSAlgebra of S1;
let OU1, OU2 be OSSubAlgebra of OU0;
clusterOU1 /\ OU2 ->  order-sorted ;
coherence
 OU1 /\ OU2 is order-sorted
proofend;
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;
func GenOSAlg A ->  strict OSSubAlgebra of OU0 means :Def12: :: OSALG_2:def 12
( A is OSSubset of it &amp; ( for OU1 being OSSubAlgebra of OU0 st A is OSSubset of OU1 holds
it is OSSubAlgebra of OU1 ) );
existence
 ex b1 being strict OSSubAlgebra of OU0 st
( A is OSSubset of b1 &amp; ( for OU1 being OSSubAlgebra of OU0 st A is OSSubset of OU1 holds
b1 is OSSubAlgebra of OU1 ) )
proofend;
uniqueness
 for b1, b2 being strict OSSubAlgebra of OU0 st A is OSSubset of b1 &amp; ( for OU1 being OSSubAlgebra of OU0 st A is OSSubset of OU1 holds
b1 is OSSubAlgebra of OU1 ) &amp; A is OSSubset of b2 &amp; ( for OU1 being OSSubAlgebra of OU0 st A is OSSubset of OU1 holds
b2 is OSSubAlgebra of OU1 ) holds
b1 = b2
proofend;
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 b4 being strict OSSubAlgebra of OU0 holds
( b4 = GenOSAlg A iff ( A is OSSubset of b4 &amp; ( for OU1 being OSSubAlgebra of OU0 st A is OSSubset of OU1 holds
b4 is OSSubAlgebra of OU1 ) ) );

:: this should rather be a definition, but I want to keep
:: 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) &amp; the Sorts of (GenOSAlg A) = OSMSubSort A )
proofend;

:: 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) &amp; the Sorts of (GenMSAlg A) = MSSubSort A )
proofend;

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)
proofend;

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;

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
proofend;

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
proofend;

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)
proofend;

definition
let S1 be OrderSortedSign;
let U0 be non-empty OSAlgebra of S1;
let U1, U2 be OSSubAlgebra of U0;
funcU1 "\/"_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
 ex b1 being strict OSSubAlgebra of U0 st
for A being OSSubset of U0 st A = the Sorts of U1 \/ the Sorts of U2 holds
b1 = GenOSAlg A
proofend;
uniqueness
 for b1, b2 being strict OSSubAlgebra of U0 st ( for A being OSSubset of U0 st A = the Sorts of U1 \/ the Sorts of U2 holds
b1 = GenOSAlg A ) &amp; ( for A being OSSubset of U0 st A = the Sorts of U1 \/ the Sorts of U2 holds
b2 = GenOSAlg A ) holds
b1 = b2
proofend;
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 b5 being strict OSSubAlgebra of U0 holds
( b5 = U1 "\/"_os U2 iff for A being OSSubset of U0 st A = the Sorts of U1 \/ the Sorts of U2 holds
b5 = GenOSAlg A );

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
proofend;

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
proofend;

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
proofend;

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
proofend;

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
proofend;

begin

:: ossub, ossubalgebra
definition
let S1 be OrderSortedSign;
let OU0 be OSAlgebra of S1;
func OSSub OU0 ->  set  means :Def14: :: OSALG_2:def 14
 for x being set holds
( x in it iff x is strict OSSubAlgebra of OU0 );
existence
 ex b1 being set st
for x being set holds
( x in b1 iff x is strict OSSubAlgebra of OU0 )
proofend;
uniqueness
 for b1, b2 being set st ( for x being set holds
( x in b1 iff x is strict OSSubAlgebra of OU0 ) ) &amp; ( for x being set holds
( x in b2 iff x is strict OSSubAlgebra of OU0 ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def14 defines OSSub OSALG_2:def_14_:_
 for S1 being OrderSortedSign
for OU0 being OSAlgebra of S1
for b3 being set holds
( b3 = OSSub OU0 iff for x being set holds
( x in b3 iff x is strict OSSubAlgebra of OU0 ) );

theorem Th42: :: OSALG_2:42
for S1 being OrderSortedSign
for OU0 being OSAlgebra of S1 holds OSSub OU0 c= MSSub OU0
proofend;

registration
let S be OrderSortedSign;
let U0 be OSAlgebra of S;
cluster OSSub U0 ->  non empty ;
coherence
 not OSSub U0 is empty
proofend;
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;

:: maybe show that e.g. for TrivialOSA(S,z,z1), OSSub(U0) is
:: proper subset of MSSub(U0), to have some counterexamples
definition
let S1 be OrderSortedSign;
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 &amp; y = U2 holds
it . (x,y) = U1 "\/"_os U2;
existence
 ex b1 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 &amp; y = U2 holds
b1 . (x,y) = U1 "\/"_os U2
proofend;
uniqueness
 for b1, b2 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 &amp; y = U2 holds
b1 . (x,y) = U1 "\/"_os U2 ) &amp; ( for x, y being Element of OSSub U0
for U1, U2 being strict OSSubAlgebra of U0 st x = U1 &amp; y = U2 holds
b2 . (x,y) = U1 "\/"_os U2 ) holds
b1 = b2
proofend;
end;

:: deftheorem Def15 defines OSAlg_join OSALG_2:def_15_:_
 for S1 being OrderSortedSign
for U0 being non-empty OSAlgebra of S1
for b3 being BinOp of (OSSub U0) holds
( b3 = OSAlg_join U0 iff for x, y being Element of OSSub U0
for U1, U2 being strict OSSubAlgebra of U0 st x = U1 &amp; y = U2 holds
b3 . (x,y) = U1 "\/"_os U2 );

definition
let S1 be OrderSortedSign;
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 &amp; y = U2 holds
it . (x,y) = U1 /\ U2;
existence
 ex b1 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 &amp; y = U2 holds
b1 . (x,y) = U1 /\ U2
proofend;
uniqueness
 for b1, b2 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 &amp; y = U2 holds
b1 . (x,y) = U1 /\ U2 ) &amp; ( for x, y being Element of OSSub U0
for U1, U2 being strict OSSubAlgebra of U0 st x = U1 &amp; y = U2 holds
b2 . (x,y) = U1 /\ U2 ) holds
b1 = b2
proofend;
end;

:: deftheorem Def16 defines OSAlg_meet OSALG_2:def_16_:_
 for S1 being OrderSortedSign
for U0 being non-empty OSAlgebra of S1
for b3 being BinOp of (OSSub U0) holds
( b3 = OSAlg_meet U0 iff for x, y being Element of OSSub U0
for U1, U2 being strict OSSubAlgebra of U0 st x = U1 &amp; y = U2 holds
b3 . (x,y) = U1 /\ U2 );

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)
proofend;

theorem Th44: :: OSALG_2:44
for S1 being OrderSortedSign
for U0 being non-empty OSAlgebra of S1 holds OSAlg_join U0 is commutative
proofend;

theorem Th45: :: OSALG_2:45
for S1 being OrderSortedSign
for U0 being non-empty OSAlgebra of S1 holds OSAlg_join U0 is associative
proofend;

theorem Th46: :: OSALG_2:46
for S1 being OrderSortedSign
for U0 being non-empty OSAlgebra of S1 holds OSAlg_meet U0 is commutative
proofend;

theorem Th47: :: OSALG_2:47
for S1 being OrderSortedSign
for U0 being non-empty OSAlgebra of S1 holds OSAlg_meet U0 is associative
proofend;

definition
let S1 be OrderSortedSign;
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) #) is strict Lattice
proofend;
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) #);

theorem Th48: :: OSALG_2:48
for S1 being OrderSortedSign
for U0 being non-empty OSAlgebra of S1 holds OSSubAlLattice U0 is bounded
proofend;

registration
let S1 be OrderSortedSign;
let U0 be non-empty OSAlgebra of S1;
cluster OSSubAlLattice U0 ->  strict bounded ;
coherence
 OSSubAlLattice U0 is bounded by Th48;
end;

theorem :: OSALG_2:49
for S1 being OrderSortedSign
for U0 being non-empty OSAlgebra of S1 holds Bottom (OSSubAlLattice U0) = GenOSAlg (OSConstants U0)
proofend;

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
proofend;

theorem :: OSALG_2:51
for S1 being OrderSortedSign
for U0 being strict non-empty OSAlgebra of S1 holds Top (OSSubAlLattice U0) = U0
proofend;