:: OSALG_2 semantic presentation

begin


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
proof
let R be non empty Poset; ::_thesis: for X, Y being OrderSortedSet of R holds X /\ Y is OrderSortedSet of R
let X, Y be OrderSortedSet of R; ::_thesis: X /\ Y is OrderSortedSet of R
reconsider M = X /\ Y as ManySortedSet of R ;
 M is order-sorted
proof
let s1, s2 be Element of R; :: according to OSALG_1:def_16 ::_thesis: ( not s1 <= s2 or M . s1 c= M . s2 )
assume  s1 <= s2 ; ::_thesis: M . s1 c= M . s2
then A1: ( X . s1 c= X . s2 & Y . s1 c= Y . s2 ) by OSALG_1:def_16;
 ( (X /\ Y) . s1 = (X . s1) /\ (Y . s1) & (X /\ Y) . s2 = (X . s2) /\ (Y . s2) ) by PBOOLE:def_5;
hence  M . s1 c= M . s2 by A1, XBOOLE_1:27; ::_thesis: verum
end;
hence  X /\ Y is OrderSortedSet of R ; ::_thesis: verum
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
proof
let R be non empty Poset; ::_thesis: for X, Y being OrderSortedSet of R holds X \/ Y is OrderSortedSet of R
let X, Y be OrderSortedSet of R; ::_thesis: X \/ Y is OrderSortedSet of R
reconsider M = X \/ Y as ManySortedSet of R ;
 M is order-sorted
proof
let s1, s2 be Element of R; :: according to OSALG_1:def_16 ::_thesis: ( not s1 <= s2 or M . s1 c= M . s2 )
assume  s1 <= s2 ; ::_thesis: M . s1 c= M . s2
then A1: ( X . s1 c= X . s2 & Y . s1 c= Y . s2 ) by OSALG_1:def_16;
 ( (X \/ Y) . s1 = (X . s1) \/ (Y . s1) & (X \/ Y) . s2 = (X . s2) \/ (Y . s2) ) by PBOOLE:def_4;
hence  M . s1 c= M . s2 by A1, XBOOLE_1:13; ::_thesis: verum
end;
hence  X \/ Y is OrderSortedSet of R ; ::_thesis: verum
end;

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
proof
reconsider X = M as ManySortedSubset of M by PBOOLE:def_18;
take  X ; ::_thesis: X is OrderSortedSet of R
thus  X is OrderSortedSet of R ; ::_thesis: verum
end;
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()
proof
reconsider N = M as ManySortedSubset of M by PBOOLE:def_18;
reconsider N1 = N as OrderSortedSubset of M by Def1;
take  N1 ; ::_thesis: N1 is V8()
thus  N1 is V8() ; ::_thesis: verum
end;
end;

begin

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
proof
reconsider B = the Sorts of U0 as MSSubset of U0 by PBOOLE:def_18;
take  B ; ::_thesis: B is OrderSortedSet of S
thus  B is OrderSortedSet of S by OSALG_1:17; ::_thesis: verum
end;
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 );

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 )
proof
set z1 = the Element of {{}};
take  TrivialOSA (S,{{}}, the Element of {{}}) ; ::_thesis: ( TrivialOSA (S,{{}}, the Element of {{}}) is monotone & TrivialOSA (S,{{}}, the Element of {{}}) is strict & TrivialOSA (S,{{}}, the Element of {{}}) is non-empty )
thus  ( TrivialOSA (S,{{}}, the Element of {{}}) is monotone & TrivialOSA (S,{{}}, the Element of {{}}) is strict & TrivialOSA (S,{{}}, the Element of {{}}) is non-empty ) ; ::_thesis: verum
end;
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()
proof
reconsider N = the Sorts of U0 as MSSubset of U0 by PBOOLE:def_18;
 the Sorts of U0 is OrderSortedSet of S by OSALG_1:17;
then reconsider M = N as OSSubset of U0 by Def2;
take  M ; ::_thesis: M is V8()
thus  M is V8() ; ::_thesis: verum
end;
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
let S0 be non empty non void strict all-with_const_op ManySortedSign ; ::_thesis: OSSign S0 is all-with_const_op
let s be Element of (OSSign S0); :: according to MSUALG_2:def_2 ::_thesis: s is with_const_op
reconsider s1 = s as Element of S0 by OSALG_1:def_5;
 s1 is with_const_op by MSUALG_2:def_2;
then consider o being Element of the carrier' of S0 such that
A1: ( the Arity of S0 . o = {} & the ResultSort of S0 . o = s1 ) by MSUALG_2:def_1;
A2: o is Element of the carrier' of (OSSign S0) by OSALG_1:def_5;
 ( the Arity of (OSSign S0) . o = {} & the ResultSort of (OSSign S0) . o = s1 ) by A1, OSALG_1:def_5;
hence  s is with_const_op by A2, MSUALG_2:def_1; ::_thesis: verum
end;

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 )
proof
set S0 = the non empty non void strict all-with_const_op ManySortedSign ;
take  OSSign the non empty non void strict all-with_const_op ManySortedSign ; ::_thesis: ( OSSign the non empty non void strict all-with_const_op ManySortedSign is all-with_const_op & OSSign the non empty non void strict all-with_const_op ManySortedSign is strict )
thus  ( OSSign the non empty non void strict all-with_const_op ManySortedSign is all-with_const_op & OSSign the non empty non void strict all-with_const_op ManySortedSign is strict ) by Th3; ::_thesis: verum
end;
end;

begin

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
proof
let S be OrderSortedSign; ::_thesis: for U0 being OSAlgebra of S holds MSAlgebra(# the Sorts of U0, the Charact of U0 #) is order-sorted
let U0 be OSAlgebra of S; ::_thesis: MSAlgebra(# the Sorts of U0, the Charact of U0 #) is order-sorted
 the Sorts of U0 is OrderSortedSet of S by OSALG_1:17;
hence  MSAlgebra(# the Sorts of U0, the Charact of U0 #) is order-sorted by OSALG_1:17; ::_thesis: verum
end;

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
proof
reconsider U1 = MSAlgebra(# the Sorts of U0, the Charact of U0 #) as strict MSSubAlgebra of U0 by MSUALG_2:37;
take  U1 ; ::_thesis: U1 is order-sorted
thus  U1 is order-sorted by Th4; ::_thesis: verum
end;
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
proof
reconsider U1 = MSAlgebra(# the Sorts of U0, the Charact of U0 #) as order-sorted MSSubAlgebra of U0 by Th4, MSUALG_2:37;
take  U1 ; ::_thesis: U1 is strict
thus  U1 is strict ; ::_thesis: verum
end;
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 )
proof
set U1 = MSAlgebra(# the Sorts of U0, the Charact of U0 #);
 the Sorts of U0 is OrderSortedSet of S by OSALG_1:17;
then reconsider U1 = MSAlgebra(# the Sorts of U0, the Charact of U0 #) as strict OSSubAlgebra of U0 by MSUALG_2:37, OSALG_1:17;
take  U1 ; ::_thesis: ( U1 is non-empty & U1 is strict )
thus  ( U1 is non-empty & U1 is strict ) ; ::_thesis: verum
end;
end;

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) ) ) ) )
proof
let S be OrderSortedSign; ::_thesis: 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) ) ) ) )
let U0 be OSAlgebra of S; ::_thesis: 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) ) ) ) )
let U1 be MSAlgebra over S; ::_thesis: ( 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) ) ) ) )
hereby  ::_thesis: ( 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) ) ) implies U1 is OSSubAlgebra of U0 )
assume A1: U1 is OSSubAlgebra of U0 ; ::_thesis: ( 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) ) ) )
then  ( the Sorts of U1 is OrderSortedSet of S & the Sorts of U1 is MSSubset of U0 ) by MSUALG_2:def_9, OSALG_1:17;
hence  the Sorts of U1 is OSSubset of U0 by Def2; ::_thesis: for B being OSSubset of U0 st B = the Sorts of U1 holds
( B is opers_closed & the Charact of U1 = Opers (U0,B) )
let B be OSSubset of U0; ::_thesis: ( B = the Sorts of U1 implies ( B is opers_closed & the Charact of U1 = Opers (U0,B) ) )
assume  B = the Sorts of U1 ; ::_thesis: ( B is opers_closed & the Charact of U1 = Opers (U0,B) )
hence  ( B is opers_closed & the Charact of U1 = Opers (U0,B) ) by A1, MSUALG_2:def_9; ::_thesis: verum
end;
assume A2: the Sorts of U1 is OSSubset of U0 ; ::_thesis: ( ex B being OSSubset of U0 st
( B = the Sorts of U1 & not ( B is opers_closed & the Charact of U1 = Opers (U0,B) ) ) or U1 is OSSubAlgebra of U0 )
assume A3: for B being OSSubset of U0 st B = the Sorts of U1 holds
( B is opers_closed & the Charact of U1 = Opers (U0,B) ) ; ::_thesis: U1 is OSSubAlgebra of U0
A4: U1 is MSSubAlgebra of U0
proof
thus  the Sorts of U1 is MSSubset of U0 by A2; :: according to MSUALG_2:def_9 ::_thesis: for b1 being ManySortedSubset of the Sorts of U0 holds
( not b1 = the Sorts of U1 or ( b1 is opers_closed & the Charact of U1 = Opers (U0,b1) ) )
let B be MSSubset of U0; ::_thesis: ( not B = the Sorts of U1 or ( B is opers_closed & the Charact of U1 = Opers (U0,B) ) )
assume A5: B = the Sorts of U1 ; ::_thesis: ( B is opers_closed & the Charact of U1 = Opers (U0,B) )
reconsider B1 = B as OSSubset of U0 by A2, A5;
 B1 is opers_closed by A3, A5;
hence  ( B is opers_closed & the Charact of U1 = Opers (U0,B) ) by A3, A5; ::_thesis: verum
end;
 the Sorts of U1 is OrderSortedSet of S by A2, Def2;
hence  U1 is OSSubAlgebra of U0 by A4, OSALG_1:17; ::_thesis: verum
end;


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)
proof
set Cs =  {  (Constants (OU0,s2)) where s2 is SortSymbol of S1 : s2 <= s  }  ;
 for X being set st X in  {  (Constants (OU0,s2)) where s2 is SortSymbol of S1 : s2 <= s  }  holds
X c= the Sorts of OU0 . s
proof
let X be set ; ::_thesis: ( X in  {  (Constants (OU0,s2)) where s2 is SortSymbol of S1 : s2 <= s  }  implies X c= the Sorts of OU0 . s )
assume  X in  {  (Constants (OU0,s2)) where s2 is SortSymbol of S1 : s2 <= s  }  ; ::_thesis: X c= the Sorts of OU0 . s
then consider s2 being SortSymbol of S1 such that
A1: X = Constants (OU0,s2) and
A2: s2 <= s ;
 the Sorts of OU0 . s2 c= the Sorts of OU0 . s by A2, OSALG_1:def_17;
hence  X c= the Sorts of OU0 . s by A1, XBOOLE_1:1; ::_thesis: verum
end;
hence  union  {  (Constants (OU0,s2)) where s2 is SortSymbol of S1 : s2 <= s  }  is Subset of ( the Sorts of OU0 . s) by ZFMISC_1:76; ::_thesis: verum
end;
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  }  ;

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)
proof
let S1 be OrderSortedSign; ::_thesis: for OU0 being OSAlgebra of S1
for s being SortSymbol of S1 holds Constants (OU0,s) c= OSConstants (OU0,s)
let OU0 be OSAlgebra of S1; ::_thesis: for s being SortSymbol of S1 holds Constants (OU0,s) c= OSConstants (OU0,s)
let s be SortSymbol of S1; ::_thesis: Constants (OU0,s) c= OSConstants (OU0,s)
 Constants (OU0,s) in  {  (Constants (OU0,s2)) where s2 is SortSymbol of S1 : s2 <= s  }  ;
hence  Constants (OU0,s) c= OSConstants (OU0,s) by ZFMISC_1:74; ::_thesis: verum
end;

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  }
proof
deffunc H1( Element of S1) ->  set = union  {  (M . s1) where s1 is SortSymbol of S1 : s1 <= $1  }  ;
consider f being Function such that
A1: ( dom f = the carrier of S1 & ( for d being Element of S1 holds f . d = H1(d) ) ) from FUNCT_1:sch_4();
reconsider f = f as ManySortedSet of the carrier of S1 by A1, PARTFUN1:def_2, RELAT_1:def_18;
reconsider f1 = f as ManySortedSet of S1 ;
 f1 is order-sorted
proof
let r1, r2 be Element of S1; :: according to OSALG_1:def_16 ::_thesis: ( not r1 <= r2 or f1 . r1 c= f1 . r2 )
assume A2: r1 <= r2 ; ::_thesis: f1 . r1 c= f1 . r2
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in f1 . r1 or x in f1 . r2 )
assume  x in f1 . r1 ; ::_thesis: x in f1 . r2
then  x in union  {  (M . s2) where s2 is SortSymbol of S1 : s2 <= r1  }  by A1;
then consider y being set  such that
A3: ( x in y & y in  {  (M . s2) where s2 is SortSymbol of S1 : s2 <= r1  }  ) by TARSKI:def_4;
consider s3 being SortSymbol of S1 such that
A4: y = M . s3 and
A5: s3 <= r1 by A3;
 s3 <= r2 by A2, A5, ORDERS_2:3;
then  y in  {  (M . s2) where s2 is SortSymbol of S1 : s2 <= r2  }  by A4;
then  x in union  {  (M . s2) where s2 is SortSymbol of S1 : s2 <= r2  }  by A3, TARSKI:def_4;
hence  x in f1 . r2 by A1; ::_thesis: verum
end;
then reconsider f2 = f1 as OrderSortedSet of S1 ;
take  f2 ; ::_thesis: for s being SortSymbol of S1 holds f2 . s = union  {  (M . s1) where s1 is SortSymbol of S1 : s1 <= s  }
thus  for s being SortSymbol of S1 holds f2 . s = union  {  (M . s1) where s1 is SortSymbol of S1 : s1 <= s  }  by A1; ::_thesis: verum
end;
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  }  ) & ( for s being SortSymbol of S1 holds b2 . s = union  {  (M . s1) where s1 is SortSymbol of S1 : s1 <= s  }  ) holds
b1 = b2
proof
let W1, W2 be OrderSortedSet of S1; ::_thesis: ( ( for s being SortSymbol of S1 holds W1 . s = union  {  (M . s1) where s1 is SortSymbol of S1 : s1 <= s  }  ) & ( for s being SortSymbol of S1 holds W2 . s = union  {  (M . s1) where s1 is SortSymbol of S1 : s1 <= s  }  ) implies W1 = W2 )
assume A6: for s being SortSymbol of S1 holds W1 . s = union  {  (M . s1) where s1 is SortSymbol of S1 : s1 <= s  }  ; ::_thesis: ( ex s being SortSymbol of S1 st not W2 . s = union  {  (M . s1) where s1 is SortSymbol of S1 : s1 <= s  }  or W1 = W2 )
assume A7: for s being SortSymbol of S1 holds W2 . s = union  {  (M . s1) where s1 is SortSymbol of S1 : s1 <= s  }  ; ::_thesis: W1 = W2
 for s being set st s in the carrier of S1 holds
W1 . s = W2 . s
proof
let s be set ; ::_thesis: ( s in the carrier of S1 implies W1 . s = W2 . s )
assume  s in the carrier of S1 ; ::_thesis: W1 . s = W2 . s
then reconsider t = s as SortSymbol of S1 ;
W1 . s = union  {  (M . s1) where s1 is SortSymbol of S1 : s1 <= t  }  by A6
.= W2 . s by A7 ;
hence  W1 . s = W2 . s ; ::_thesis: verum
end;
hence  W1 = W2 by PBOOLE:3; ::_thesis: verum
end;
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
proof
let S1 be OrderSortedSign; ::_thesis: for M being ManySortedSet of the carrier of S1 holds M c= OSCl M
let M be ManySortedSet of the carrier of S1; ::_thesis: M c= OSCl M
let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in the carrier of S1 or M . i c= (OSCl M) . i )
assume  i in the carrier of S1 ; ::_thesis: M . i c= (OSCl M) . i
then reconsider s = i as SortSymbol of S1 ;
 M . s in  {  (M . s1) where s1 is SortSymbol of S1 : s1 <= s  }  ;
then  M . s c= union  {  (M . s1) where s1 is SortSymbol of S1 : s1 <= s  }  by ZFMISC_1:74;
hence  M . i c= (OSCl M) . i by Def4; ::_thesis: verum
end;

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
proof
let S1 be OrderSortedSign; ::_thesis: for M being ManySortedSet of the carrier of S1
for A being OrderSortedSet of S1 st M c= A holds
OSCl M c= A
let M be ManySortedSet of the carrier of S1; ::_thesis: for A being OrderSortedSet of S1 st M c= A holds
OSCl M c= A
let A be OrderSortedSet of S1; ::_thesis: ( M c= A implies OSCl M c= A )
assume A1: M c= A ; ::_thesis: OSCl M c= A
assume  not OSCl M c= A ; ::_thesis: contradiction
then consider i being set  such that
A2: i in the carrier of S1 and
A3: not (OSCl M) . i c= A . i by PBOOLE:def_2;
reconsider s = i as SortSymbol of S1 by A2;
consider x being set  such that
A4: x in (OSCl M) . i and
A5: not x in A . i by A3, TARSKI:def_3;
 (OSCl M) . s = union  {  (M . s2) where s2 is SortSymbol of S1 : s2 <= s  }  by Def4;
then consider X1 being set  such that
A6: x in X1 and
A7: X1 in  {  (M . s2) where s2 is SortSymbol of S1 : s2 <= s  }  by A4, TARSKI:def_4;
consider s1 being SortSymbol of S1 such that
A8: X1 = M . s1 and
A9: s1 <= s by A7;
 M . s1 c= A . s1 by A1, PBOOLE:def_2;
then A10: x in A . s1 by A6, A8;
 A . s1 c= A . s by A9, OSALG_1:def_16;
hence  contradiction by A5, A10; ::_thesis: verum
end;

theorem :: OSALG_2:9
for S being OrderSortedSign
for X being OrderSortedSet of S holds OSCl X = X
proof
let S be OrderSortedSign; ::_thesis: for X being OrderSortedSet of S holds OSCl X = X
let X be OrderSortedSet of S; ::_thesis: OSCl X = X
 ( X c= OSCl X & OSCl X c= X ) by Th7, Th8;
hence  OSCl X = X by PBOOLE:146; ::_thesis: verum
end;

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)
proof
deffunc H1( Element of S1) ->  set = union  {  (Constants (OU0,s1)) where s1 is SortSymbol of S1 : s1 <= $1  }  ;
consider f being Function such that
A1: ( dom f = the carrier of S1 & ( for d being Element of S1 holds f . d = H1(d) ) ) from FUNCT_1:sch_4();
reconsider f = f as ManySortedSet of the carrier of S1 by A1, PARTFUN1:def_2, RELAT_1:def_18;
 f c= the Sorts of OU0
proof
let s be set ; :: according to PBOOLE:def_2 ::_thesis: ( not s in the carrier of S1 or f . s c= the Sorts of OU0 . s )
assume  s in the carrier of S1 ; ::_thesis: f . s c= the Sorts of OU0 . s
then reconsider s1 = s as SortSymbol of S1 ;
 f . s1 = OSConstants (OU0,s1) by A1;
hence  f . s c= the Sorts of OU0 . s ; ::_thesis: verum
end;
then reconsider f = f as MSSubset of OU0 by PBOOLE:def_18;
take  f ; ::_thesis: ( f is OSSubset of OU0 & ( for s being SortSymbol of S1 holds f . s = OSConstants (OU0,s) ) )
reconsider f1 = f as ManySortedSet of S1 ;
 f1 is order-sorted
proof
let r1, r2 be Element of S1; :: according to OSALG_1:def_16 ::_thesis: ( not r1 <= r2 or f1 . r1 c= f1 . r2 )
assume A2: r1 <= r2 ; ::_thesis: f1 . r1 c= f1 . r2
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in f1 . r1 or x in f1 . r2 )
assume  x in f1 . r1 ; ::_thesis: x in f1 . r2
then  x in union  {  (Constants (OU0,s2)) where s2 is SortSymbol of S1 : s2 <= r1  }  by A1;
then consider y being set  such that
A3: ( x in y & y in  {  (Constants (OU0,s2)) where s2 is SortSymbol of S1 : s2 <= r1  }  ) by TARSKI:def_4;
consider s3 being SortSymbol of S1 such that
A4: y = Constants (OU0,s3) and
A5: s3 <= r1 by A3;
 s3 <= r2 by A2, A5, ORDERS_2:3;
then  y in  {  (Constants (OU0,s2)) where s2 is SortSymbol of S1 : s2 <= r2  }  by A4;
then  x in union  {  (Constants (OU0,s2)) where s2 is SortSymbol of S1 : s2 <= r2  }  by A3, TARSKI:def_4;
hence  x in f1 . r2 by A1; ::_thesis: verum
end;
hence  f is OSSubset of OU0 by Def2; ::_thesis: for s being SortSymbol of S1 holds f . s = OSConstants (OU0,s)
thus  for s being SortSymbol of S1 holds f . s = OSConstants (OU0,s) by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being OSSubset of OU0 st ( for s being SortSymbol of S1 holds b1 . s = OSConstants (OU0,s) ) & ( for s being SortSymbol of S1 holds b2 . s = OSConstants (OU0,s) ) holds
b1 = b2
proof
let W1, W2 be OSSubset of OU0; ::_thesis: ( ( for s being SortSymbol of S1 holds W1 . s = OSConstants (OU0,s) ) & ( for s being SortSymbol of S1 holds W2 . s = OSConstants (OU0,s) ) implies W1 = W2 )
assume that
A6: for s being SortSymbol of S1 holds W1 . s = OSConstants (OU0,s) and
A7: for s being SortSymbol of S1 holds W2 . s = OSConstants (OU0,s) ; ::_thesis: W1 = W2
 for s being set st s in the carrier of S1 holds
W1 . s = W2 . s
proof
let s be set ; ::_thesis: ( s in the carrier of S1 implies W1 . s = W2 . s )
assume  s in the carrier of S1 ; ::_thesis: W1 . s = W2 . s
then reconsider t = s as SortSymbol of S1 ;
 W1 . t = OSConstants (OU0,t) by A6;
hence  W1 . s = W2 . s by A7; ::_thesis: verum
end;
hence  W1 = W2 by PBOOLE:3; ::_thesis: verum
end;
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
proof
let S1 be OrderSortedSign; ::_thesis: for OU0 being OSAlgebra of S1 holds Constants OU0 c= OSConstants OU0
let OU0 be OSAlgebra of S1; ::_thesis: Constants OU0 c= OSConstants OU0
let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in the carrier of S1 or (Constants OU0) . i c= (OSConstants OU0) . i )
assume  i in the carrier of S1 ; ::_thesis: (Constants OU0) . i c= (OSConstants OU0) . i
then reconsider s = i as SortSymbol of S1 ;
 ( (Constants OU0) . s = Constants (OU0,s) & (OSConstants OU0) . s = OSConstants (OU0,s) ) by Def5, MSUALG_2:def_4;
hence  (Constants OU0) . i c= (OSConstants OU0) . i by Th6; ::_thesis: verum
end;

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
proof
let S1 be OrderSortedSign; ::_thesis: for OU0 being OSAlgebra of S1
for A being OSSubset of OU0 st Constants OU0 c= A holds
OSConstants OU0 c= A
let OU0 be OSAlgebra of S1; ::_thesis: for A being OSSubset of OU0 st Constants OU0 c= A holds
OSConstants OU0 c= A
let A be OSSubset of OU0; ::_thesis: ( Constants OU0 c= A implies OSConstants OU0 c= A )
assume A1: Constants OU0 c= A ; ::_thesis: OSConstants OU0 c= A
assume  not OSConstants OU0 c= A ; ::_thesis: contradiction
then consider i being set  such that
A2: i in the carrier of S1 and
A3: not (OSConstants OU0) . i c= A . i by PBOOLE:def_2;
reconsider s = i as SortSymbol of S1 by A2;
consider x being set  such that
A4: x in (OSConstants OU0) . i and
A5: not x in A . i by A3, TARSKI:def_3;
(OSConstants OU0) . s = OSConstants (OU0,s) by Def5
.= union  {  (Constants (OU0,s2)) where s2 is SortSymbol of S1 : s2 <= s  }  ;
then consider X1 being set  such that
A6: x in X1 and
A7: X1 in  {  (Constants (OU0,s2)) where s2 is SortSymbol of S1 : s2 <= s  }  by A4, TARSKI:def_4;
consider s1 being SortSymbol of S1 such that
A8: X1 = Constants (OU0,s1) and
A9: s1 <= s by A7;
A10: (Constants OU0) . s1 c= A . s1 by A1, PBOOLE:def_2;
 x in (Constants OU0) . s1 by A6, A8, MSUALG_2:def_4;
then A11: x in A . s1 by A10;
 A is OrderSortedSet of S1 by Def2;
then  A . s1 c= A . s by A9, OSALG_1:def_16;
hence  contradiction by A5, A11; ::_thesis: verum
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)
proof
let S1 be OrderSortedSign; ::_thesis: for OU0 being OSAlgebra of S1
for A being OSSubset of OU0 holds OSConstants OU0 = OSCl (Constants OU0)
let OU0 be OSAlgebra of S1; ::_thesis: for A being OSSubset of OU0 holds OSConstants OU0 = OSCl (Constants OU0)
let A be OSSubset of OU0; ::_thesis: OSConstants OU0 = OSCl (Constants OU0)
A1: now__::_thesis:_for_i_being_set_st_i_in_the_carrier_of_S1_holds_
(OSConstants_OU0)_._i_=_(OSCl_(Constants_OU0))_._i
let i be set ; ::_thesis: ( i in the carrier of S1 implies (OSConstants OU0) . i = (OSCl (Constants OU0)) . i )
assume  i in the carrier of S1 ; ::_thesis: (OSConstants OU0) . i = (OSCl (Constants OU0)) . i
then reconsider s = i as SortSymbol of S1 ;
set c1 =  {  ((Constants OU0) . s1) where s1 is SortSymbol of S1 : s1 <= s  }  ;
set c2 =  {  (Constants (OU0,s1)) where s1 is SortSymbol of S1 : s1 <= s  }  ;
 for x being set holds
( x in  {  ((Constants OU0) . s1) where s1 is SortSymbol of S1 : s1 <= s  }  iff x in  {  (Constants (OU0,s1)) where s1 is SortSymbol of S1 : s1 <= s  }  )
proof
let x be set ; ::_thesis: ( x in  {  ((Constants OU0) . s1) where s1 is SortSymbol of S1 : s1 <= s  }  iff x in  {  (Constants (OU0,s1)) where s1 is SortSymbol of S1 : s1 <= s  }  )
hereby  ::_thesis: ( x in  {  (Constants (OU0,s1)) where s1 is SortSymbol of S1 : s1 <= s  }  implies x in  {  ((Constants OU0) . s1) where s1 is SortSymbol of S1 : s1 <= s  }  )
assume  x in  {  ((Constants OU0) . s1) where s1 is SortSymbol of S1 : s1 <= s  }  ; ::_thesis: x in  {  (Constants (OU0,s1)) where s1 is SortSymbol of S1 : s1 <= s  }
then consider s1 being SortSymbol of S1 such that
A2: x = (Constants OU0) . s1 and
A3: s1 <= s ;
 x = Constants (OU0,s1) by A2, MSUALG_2:def_4;
hence  x in  {  (Constants (OU0,s1)) where s1 is SortSymbol of S1 : s1 <= s  }  by A3; ::_thesis: verum
end;
assume  x in  {  (Constants (OU0,s1)) where s1 is SortSymbol of S1 : s1 <= s  }  ; ::_thesis: x in  {  ((Constants OU0) . s1) where s1 is SortSymbol of S1 : s1 <= s  }
then consider s1 being SortSymbol of S1 such that
A4: x = Constants (OU0,s1) and
A5: s1 <= s ;
 x = (Constants OU0) . s1 by A4, MSUALG_2:def_4;
hence  x in  {  ((Constants OU0) . s1) where s1 is SortSymbol of S1 : s1 <= s  }  by A5; ::_thesis: verum
end;
then A6:  {  ((Constants OU0) . s1) where s1 is SortSymbol of S1 : s1 <= s  }  =  {  (Constants (OU0,s1)) where s1 is SortSymbol of S1 : s1 <= s  }  by TARSKI:1;
(OSConstants OU0) . s = OSConstants (OU0,s) by Def5
.= (OSCl (Constants OU0)) . s by A6, Def4 ;
hence  (OSConstants OU0) . i = (OSCl (Constants OU0)) . i ; ::_thesis: verum
end;
then  for i being set st i in the carrier of S1 holds
(OSCl (Constants OU0)) . i c= (OSConstants OU0) . i ;
then A7: OSCl (Constants OU0) c= OSConstants OU0 by PBOOLE:def_2;
 for i being set st i in the carrier of S1 holds
(OSConstants OU0) . i c= (OSCl (Constants OU0)) . i by A1;
then  OSConstants OU0 c= OSCl (Constants OU0) by PBOOLE:def_2;
hence  OSConstants OU0 = OSCl (Constants OU0) by A7, PBOOLE:146; ::_thesis: verum
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
proof
let S1 be OrderSortedSign; ::_thesis: for OU0 being OSAlgebra of S1
for OU1 being OSSubAlgebra of OU0 holds OSConstants OU0 is OSSubset of OU1
let OU0 be OSAlgebra of S1; ::_thesis: for OU1 being OSSubAlgebra of OU0 holds OSConstants OU0 is OSSubset of OU1
let OU1 be OSSubAlgebra of OU0; ::_thesis: OSConstants OU0 is OSSubset of OU1
 OSConstants OU0 c= the Sorts of OU1
proof
let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in the carrier of S1 or (OSConstants OU0) . i c= the Sorts of OU1 . i )
assume  i in the carrier of S1 ; ::_thesis: (OSConstants OU0) . i c= the Sorts of OU1 . i
then reconsider s = i as SortSymbol of S1 ;
 Constants OU0 is MSSubset of OU1 by MSUALG_2:10;
then A1: Constants OU0 c= the Sorts of OU1 by PBOOLE:def_18;
A2: for s2, s3 being SortSymbol of S1 st s2 <= s3 holds
(Constants OU0) . s2 c= the Sorts of OU1 . s3
proof
let s2, s3 be SortSymbol of S1; ::_thesis: ( s2 <= s3 implies (Constants OU0) . s2 c= the Sorts of OU1 . s3 )
assume  s2 <= s3 ; ::_thesis: (Constants OU0) . s2 c= the Sorts of OU1 . s3
then A3: the Sorts of OU1 . s2 c= the Sorts of OU1 . s3 by OSALG_1:def_17;
 (Constants OU0) . s2 c= the Sorts of OU1 . s2 by A1, PBOOLE:def_2;
hence  (Constants OU0) . s2 c= the Sorts of OU1 . s3 by A3, XBOOLE_1:1; ::_thesis: verum
end;
A4: for X being set st X in  {  (Constants (OU0,s1)) where s1 is SortSymbol of S1 : s1 <= s  }  holds
X c= the Sorts of OU1 . s
proof
let X be set ; ::_thesis: ( X in  {  (Constants (OU0,s1)) where s1 is SortSymbol of S1 : s1 <= s  }  implies X c= the Sorts of OU1 . s )
assume  X in  {  (Constants (OU0,s1)) where s1 is SortSymbol of S1 : s1 <= s  }  ; ::_thesis: X c= the Sorts of OU1 . s
then consider s4 being SortSymbol of S1 such that
A5: ( X = Constants (OU0,s4) & s4 <= s ) ;
 Constants (OU0,s4) = (Constants OU0) . s4 by MSUALG_2:def_4;
hence  X c= the Sorts of OU1 . s by A2, A5; ::_thesis: verum
end;
(OSConstants OU0) . i = OSConstants (OU0,s) by Def5
.= union  {  (Constants (OU0,s1)) where s1 is SortSymbol of S1 : s1 <= s  }  ;
hence  (OSConstants OU0) . i c= the Sorts of OU1 . i by A4, ZFMISC_1:76; ::_thesis: verum
end;
then A6: OSConstants OU0 is ManySortedSubset of the Sorts of OU1 by PBOOLE:def_18;
 OSConstants OU0 is OrderSortedSet of S1 by Def2;
hence  OSConstants OU0 is OSSubset of OU1 by A6, Def2; ::_thesis: verum
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
proof
let S be all-with_const_op OrderSortedSign; ::_thesis: for OU0 being non-empty OSAlgebra of S
for OU1 being non-empty OSSubAlgebra of OU0 holds OSConstants OU0 is V8() OSSubset of OU1
let OU0 be non-empty OSAlgebra of S; ::_thesis: for OU1 being non-empty OSSubAlgebra of OU0 holds OSConstants OU0 is V8() OSSubset of OU1
let OU1 be non-empty OSSubAlgebra of OU0; ::_thesis: OSConstants OU0 is V8() OSSubset of OU1
 Constants OU0 c= OSConstants OU0 by Th10;
hence  OSConstants OU0 is V8() OSSubset of OU1 by Th13, PBOOLE:131; ::_thesis: verum
end;

begin

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) )
proof
let I be set ; ::_thesis: for M being ManySortedSet of I
for x being set holds
( x is ManySortedSubset of M iff x in product (bool M) )
let M be ManySortedSet of I; ::_thesis: for x being set holds
( x is ManySortedSubset of M iff x in product (bool M) )
let x be set ; ::_thesis: ( x is ManySortedSubset of M iff x in product (bool M) )
A1: I = dom (bool M) by PARTFUN1:def_2;
hereby  ::_thesis: ( x in product (bool M) implies x is ManySortedSubset of M )
assume  x is ManySortedSubset of M ; ::_thesis: x in product (bool M)
then reconsider x1 = x as ManySortedSubset of M ;
A2: for i being set st i in dom (bool M) holds
x1 . i in (bool M) . i
proof
let i be set ; ::_thesis: ( i in dom (bool M) implies x1 . i in (bool M) . i )
assume A3: i in dom (bool M) ; ::_thesis: x1 . i in (bool M) . i
 x1 c= M by PBOOLE:def_18;
then  x1 . i c= M . i by A1, A3, PBOOLE:def_2;
then  x1 . i in bool (M . i) ;
hence  x1 . i in (bool M) . i by A1, A3, MBOOLEAN:def_1; ::_thesis: verum
end;
dom x1 = I by PARTFUN1:def_2
.= dom (bool M) by PARTFUN1:def_2 ;
hence  x in product (bool M) by A2, CARD_3:def_5; ::_thesis: verum
end;
assume  x in product (bool M) ; ::_thesis: x is ManySortedSubset of M
then consider x1 being Function such that
A4: x = x1 and
A5: dom x1 = dom (bool M) and
A6: for i being set st i in dom (bool M) holds
x1 . i in (bool M) . i by CARD_3:def_5;
 dom x1 = I by A5, PARTFUN1:def_2;
then reconsider x2 = x1 as ManySortedSet of I by PARTFUN1:def_2, RELAT_1:def_18;
 x2 c= M
proof
let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in I or x2 . i c= M . i )
assume A7: i in I ; ::_thesis: x2 . i c= M . i
 x2 . i in (bool M) . i by A1, A6, A7;
then  x2 . i in bool (M . i) by A7, MBOOLEAN:def_1;
hence  x2 . i c= M . i ; ::_thesis: verum
end;
hence  x is ManySortedSubset of M by A4, PBOOLE:def_18; ::_thesis: verum
end;

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 )
proof
defpred S1[ set ] means $1 is OrderSortedSubset of M;
set f = product (bool M);
consider X being set  such that
A1: for y being set holds
( y in X iff ( y in product (bool M) & S1[y] ) ) from XBOOLE_0:sch_1();
take  X ; ::_thesis: for x being set holds
( x in X iff x is OrderSortedSubset of M )
let y be set ; ::_thesis: ( y in X iff y is OrderSortedSubset of M )
thus  ( y in X implies y is OrderSortedSubset of M ) by A1; ::_thesis: ( y is OrderSortedSubset of M implies y in X )
assume A2: y is OrderSortedSubset of M ; ::_thesis: y in X
then  y in product (bool M) by Th15;
hence  y in X by A1, A2; ::_thesis: verum
end;
uniqueness
 for b1, b2 being set st ( for x being set holds
( x in b1 iff x is OrderSortedSubset of M ) ) & ( for x being set holds
( x in b2 iff x is OrderSortedSubset of M ) ) holds
b1 = b2
proof
defpred S1[ set ] means $1 is OrderSortedSubset of M;
thus  for X1, X2 being set st ( for x being set holds
( x in X1 iff S1[x] ) ) & ( for x being set holds
( x in X2 iff S1[x] ) ) holds
X1 = X2 from XBOOLE_0:sch_3(); ::_thesis: verum
end;
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
proof
let S1 be OrderSortedSign; ::_thesis: for OU0 being OSAlgebra of S1
for A being OSSubset of OU0 holds OSSubSort A c= SubSort A
let OU0 be OSAlgebra of S1; ::_thesis: for A being OSSubset of OU0 holds OSSubSort A c= SubSort A
let A be OSSubset of OU0; ::_thesis: OSSubSort A c= SubSort A
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in OSSubSort A or x in SubSort A )
assume  x in OSSubSort A ; ::_thesis: x in SubSort A
then  ex y being Element of SubSort A st
( x = y & y is OrderSortedSet of S1 ) ;
hence  x in SubSort A ; ::_thesis: verum
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
proof
let S1 be OrderSortedSign; ::_thesis: for OU0 being OSAlgebra of S1
for A being OSSubset of OU0 holds the Sorts of OU0 in OSSubSort A
let OU0 be OSAlgebra of S1; ::_thesis: for A being OSSubset of OU0 holds the Sorts of OU0 in OSSubSort A
let A be OSSubset of OU0; ::_thesis: the Sorts of OU0 in OSSubSort A
reconsider X = the Sorts of OU0 as Element of SubSort A by MSUALG_2:38;
 the Sorts of OU0 is OrderSortedSet of S1 by OSALG_1:17;
then  X in  {  x where x is Element of SubSort A : x is OrderSortedSet of S1  }  ;
hence  the Sorts of OU0 in OSSubSort A ; ::_thesis: verum
end;

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
proof
let S1 be OrderSortedSign; ::_thesis: for OU0 being OSAlgebra of S1
for A being OSSubset of OU0 holds OSSubSort A c= OSSubSort OU0
let OU0 be OSAlgebra of S1; ::_thesis: for A being OSSubset of OU0 holds OSSubSort A c= OSSubSort OU0
let A be OSSubset of OU0; ::_thesis: OSSubSort A c= OSSubSort OU0
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in OSSubSort A or x in OSSubSort OU0 )
assume  x in OSSubSort A ; ::_thesis: x in OSSubSort OU0
then consider x1 being Element of SubSort A such that
A1: x1 = x and
A2: x1 is OrderSortedSet of S1 ;
 ( x1 in SubSort A & SubSort A c= SubSort OU0 ) by MSUALG_2:39;
then reconsider x2 = x1 as Element of SubSort OU0 ;
 x2 in  {  y where y is Element of SubSort OU0 : y is OrderSortedSet of S1  }  by A2;
hence  x in OSSubSort OU0 by A1; ::_thesis: verum
end;

registration
let S1 be OrderSortedSign;
let OU0 be OSAlgebra of S1;
cluster OSSubSort OU0 ->  non empty ;
coherence
 not OSSubSort OU0 is empty
proof
set A = the OSSubset of OU0;
 OSSubSort the OSSubset of OU0 c= OSSubSort OU0 by Th18;
hence  not OSSubSort OU0 is empty ; ::_thesis: verum
end;
end;

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
proof
 e in  {  x where x is Element of SubSort OU0 : x is OrderSortedSet of S1  }  ;
then consider e1 being Element of SubSort OU0 such that
A1: e = e1 and
A2: e1 is OrderSortedSet of S1 ;
reconsider e2 = @ e1 as OSSubset of OU0 by A2, Def2;
 e2 = e by A1;
hence  e is OSSubset of OU0 ; ::_thesis: verum
end;
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;

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 ) )
proof
let S1 be OrderSortedSign; ::_thesis: 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 ) )
let OU0 be OSAlgebra of S1; ::_thesis: for A, B being OSSubset of OU0 holds
( B in OSSubSort A iff ( B is opers_closed & OSConstants OU0 c= B & A c= B ) )
let A, B be OSSubset of OU0; ::_thesis: ( B in OSSubSort A iff ( B is opers_closed & OSConstants OU0 c= B & A c= B ) )
thus  ( B in OSSubSort A implies ( B is opers_closed & OSConstants OU0 c= B & A c= B ) ) ::_thesis: ( B is opers_closed & OSConstants OU0 c= B & A c= B implies B in OSSubSort A )
proof
assume  B in OSSubSort A ; ::_thesis: ( B is opers_closed & OSConstants OU0 c= B & A c= B )
then A1: ex B1 being Element of SubSort A st
( B1 = B & B1 is OrderSortedSet of S1 ) ;
then  Constants OU0 c= B by MSUALG_2:13;
hence  ( B is opers_closed & OSConstants OU0 c= B & A c= B ) by A1, Th11, MSUALG_2:13; ::_thesis: verum
end;
assume that
A2: B is opers_closed and
A3: OSConstants OU0 c= B and
A4: A c= B ; ::_thesis: B in OSSubSort A
 Constants OU0 c= OSConstants OU0 by Th10;
then  Constants OU0 c= B by A3, PBOOLE:13;
then A5: B in SubSort A by A2, A4, MSUALG_2:13;
 B is OrderSortedSet of S1 by Def2;
hence  B in OSSubSort A by A5; ::_thesis: verum
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 )
proof
let S1 be OrderSortedSign; ::_thesis: for OU0 being OSAlgebra of S1
for B being OSSubset of OU0 holds
( B in OSSubSort OU0 iff B is opers_closed )
let OU0 be OSAlgebra of S1; ::_thesis: for B being OSSubset of OU0 holds
( B in OSSubSort OU0 iff B is opers_closed )
let B be OSSubset of OU0; ::_thesis: ( B in OSSubSort OU0 iff B is opers_closed )
A1: ( B in SubSort OU0 iff B is opers_closed ) by MSUALG_2:14;
thus  ( B in OSSubSort OU0 implies B is opers_closed ) ::_thesis: ( B is opers_closed implies B in OSSubSort OU0 )
proof
assume  B in OSSubSort OU0 ; ::_thesis: B is opers_closed
then  ex B1 being Element of SubSort OU0 st
( B1 = B & B1 is OrderSortedSet of S1 ) ;
hence  B is opers_closed by MSUALG_2:14; ::_thesis: verum
end;
assume A2: B is opers_closed ; ::_thesis: B in OSSubSort OU0
 B is OrderSortedSet of S1 by Def2;
hence  B in OSSubSort OU0 by A1, A2; ::_thesis: verum
end;

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 & 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 & x = B . s ) )
proof
defpred S1[ set ] means  ex B being OSSubset of OU0 st
( B in OSSubSort A & $1 = B . s );
set C = bool (Union the Sorts of OU0);
consider X being set  such that
A1: for x being set holds
( x in X iff ( x in bool (Union the Sorts of OU0) & S1[x] ) ) from XBOOLE_0:sch_1();
take  X ; ::_thesis: for x being set holds
( x in X iff ex B being OSSubset of OU0 st
( B in OSSubSort A & x = B . s ) )
A2: bool (Union the Sorts of OU0) = bool (union (rng the Sorts of OU0)) by CARD_3:def_4;
 for x being set holds
( x in X iff ex B being OSSubset of OU0 st
( B in OSSubSort A & x = B . s ) )
proof
 dom the Sorts of OU0 = the carrier of S1 by PARTFUN1:def_2;
then  the Sorts of OU0 . s in rng the Sorts of OU0 by FUNCT_1:def_3;
then A3: the Sorts of OU0 . s c= union (rng the Sorts of OU0) by ZFMISC_1:74;
let x be set ; ::_thesis: ( x in X iff ex B being OSSubset of OU0 st
( B in OSSubSort A & x = B . s ) )
thus  ( x in X implies ex B being OSSubset of OU0 st
( B in OSSubSort A & x = B . s ) ) by A1; ::_thesis: ( ex B being OSSubset of OU0 st
( B in OSSubSort A & x = B . s ) implies x in X )
given B being OSSubset of OU0 such that A4: B in OSSubSort A and
A5: x = B . s ; ::_thesis: x in X
 B c= the Sorts of OU0 by PBOOLE:def_18;
then  B . s c= the Sorts of OU0 . s by PBOOLE:def_2;
then  x c= union (rng the Sorts of OU0) by A5, A3, XBOOLE_1:1;
hence  x in X by A2, A1, A4, A5; ::_thesis: verum
end;
hence  for x being set holds
( x in X iff ex B being OSSubset of OU0 st
( B in OSSubSort A & x = B . s ) ) ; ::_thesis: verum
end;
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 & x = B . s ) ) ) & ( for x being set holds
( x in b2 iff ex B being OSSubset of OU0 st
( B in OSSubSort A & x = B . s ) ) ) holds
b1 = b2
proof
defpred S1[ set ] means  ex B being OSSubset of OU0 st
( B in OSSubSort A & $1 = B . s );
thus  for X1, X2 being set st ( for x being set holds
( x in X1 iff S1[x] ) ) & ( for x being set holds
( x in X2 iff S1[x] ) ) holds
X1 = X2 from XBOOLE_0:sch_3(); ::_thesis: verum
end;
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 & 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)
proof
let S1 be OrderSortedSign; ::_thesis: 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)
let OU0 be OSAlgebra of S1; ::_thesis: 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)
let A be OSSubset of OU0; ::_thesis: for s1, s2 being SortSymbol of S1 st s1 <= s2 holds
OSSubSort (A,s2) is_coarser_than OSSubSort (A,s1)
let s1, s2 be SortSymbol of S1; ::_thesis: ( s1 <= s2 implies OSSubSort (A,s2) is_coarser_than OSSubSort (A,s1) )
assume A1: s1 <= s2 ; ::_thesis: OSSubSort (A,s2) is_coarser_than OSSubSort (A,s1)
 for Y being set st Y in OSSubSort (A,s2) holds
ex X being set st
( X in OSSubSort (A,s1) & X c= Y )
proof
let x be set ; ::_thesis: ( x in OSSubSort (A,s2) implies ex X being set st
( X in OSSubSort (A,s1) & X c= x ) )
assume  x in OSSubSort (A,s2) ; ::_thesis: ex X being set st
( X in OSSubSort (A,s1) & X c= x )
then consider B being OSSubset of OU0 such that
A2: ( B in OSSubSort A & x = B . s2 ) by Def10;
take  B . s1 ; ::_thesis: ( B . s1 in OSSubSort (A,s1) & B . s1 c= x )
 B is OrderSortedSet of S1 by Def2;
hence  ( B . s1 in OSSubSort (A,s1) & B . s1 c= x ) by A1, A2, Def10, OSALG_1:def_16; ::_thesis: verum
end;
hence  OSSubSort (A,s2) is_coarser_than OSSubSort (A,s1) by SETFAM_1:def_3; ::_thesis: verum
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)
proof
let S1 be OrderSortedSign; ::_thesis: 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)
let OU0 be OSAlgebra of S1; ::_thesis: for A being OSSubset of OU0
for s being SortSymbol of S1 holds OSSubSort (A,s) c= SubSort (A,s)
let A be OSSubset of OU0; ::_thesis: for s being SortSymbol of S1 holds OSSubSort (A,s) c= SubSort (A,s)
let s be SortSymbol of S1; ::_thesis: OSSubSort (A,s) c= SubSort (A,s)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in OSSubSort (A,s) or x in SubSort (A,s) )
assume  x in OSSubSort (A,s) ; ::_thesis: x in SubSort (A,s)
then A1: ex B being OSSubset of OU0 st
( B in OSSubSort A & x = B . s ) by Def10;
 OSSubSort A c= SubSort A by Th16;
hence  x in SubSort (A,s) by A1, MSUALG_2:def_13; ::_thesis: verum
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)
proof
let S1 be OrderSortedSign; ::_thesis: 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)
let OU0 be OSAlgebra of S1; ::_thesis: for A being OSSubset of OU0
for s being SortSymbol of S1 holds the Sorts of OU0 . s in OSSubSort (A,s)
let A be OSSubset of OU0; ::_thesis: for s being SortSymbol of S1 holds the Sorts of OU0 . s in OSSubSort (A,s)
let s be SortSymbol of S1; ::_thesis: the Sorts of OU0 . s in OSSubSort (A,s)
 ( the Sorts of OU0 is ManySortedSubset of the Sorts of OU0 & the Sorts of OU0 is OrderSortedSet of S1 ) by OSALG_1:17, PBOOLE:def_18;
then reconsider B = the Sorts of OU0 as OSSubset of OU0 by Def2;
 the Sorts of OU0 in OSSubSort A by Th17;
then  B . s in OSSubSort (A,s) by Def10;
hence  the Sorts of OU0 . s in OSSubSort (A,s) ; ::_thesis: verum
end;

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))
proof
deffunc H1( Element of S1) ->  set = meet (OSSubSort (A,$1));
consider f being Function such that
A1: ( dom f = the carrier of S1 & ( for s being Element of S1 holds f . s = H1(s) ) ) from FUNCT_1:sch_4();
reconsider f = f as ManySortedSet of the carrier of S1 by A1, PARTFUN1:def_2, RELAT_1:def_18;
 f c= the Sorts of OU0
proof
reconsider u0 = the Sorts of OU0 as MSSubset of OU0 by PBOOLE:def_18;
let x be set ; :: according to PBOOLE:def_2 ::_thesis: ( not x in the carrier of S1 or f . x c= the Sorts of OU0 . x )
assume  x in the carrier of S1 ; ::_thesis: f . x c= the Sorts of OU0 . x
then reconsider s = x as SortSymbol of S1 ;
A2: f . s = meet (OSSubSort (A,s)) by A1;
 u0 is OrderSortedSet of S1 by OSALG_1:17;
then A3: u0 is OSSubset of OU0 by Def2;
 u0 in OSSubSort A by Th17;
then  the Sorts of OU0 . s in OSSubSort (A,s) by A3, Def10;
hence  f . x c= the Sorts of OU0 . x by A2, SETFAM_1:3; ::_thesis: verum
end;
then reconsider f = f as MSSubset of OU0 by PBOOLE:def_18;
take  f ; ::_thesis: ( f is OSSubset of OU0 & ( for s being SortSymbol of S1 holds f . s = meet (OSSubSort (A,s)) ) )
reconsider f1 = f as ManySortedSet of S1 ;
 for s1, s2 being Element of S1 st s1 <= s2 holds
f1 . s1 c= f1 . s2
proof
let s1, s2 be Element of S1; ::_thesis: ( s1 <= s2 implies f1 . s1 c= f1 . s2 )
assume  s1 <= s2 ; ::_thesis: f1 . s1 c= f1 . s2
then A4: meet (OSSubSort (A,s1)) c= meet (OSSubSort (A,s2)) by Th21, SETFAM_1:14;
 f1 . s1 = meet (OSSubSort (A,s1)) by A1;
hence  f1 . s1 c= f1 . s2 by A1, A4; ::_thesis: verum
end;
then  f is OrderSortedSet of S1 by OSALG_1:def_16;
hence  ( f is OSSubset of OU0 & ( for s being SortSymbol of S1 holds f . s = meet (OSSubSort (A,s)) ) ) by A1, Def2; ::_thesis: verum
end;
uniqueness
 for b1, b2 being OSSubset of OU0 st ( for s being SortSymbol of S1 holds b1 . s = meet (OSSubSort (A,s)) ) & ( for s being SortSymbol of S1 holds b2 . s = meet (OSSubSort (A,s)) ) holds
b1 = b2
proof
let W1, W2 be OSSubset of OU0; ::_thesis: ( ( for s being SortSymbol of S1 holds W1 . s = meet (OSSubSort (A,s)) ) & ( for s being SortSymbol of S1 holds W2 . s = meet (OSSubSort (A,s)) ) implies W1 = W2 )
assume that
A5: for s being SortSymbol of S1 holds W1 . s = meet (OSSubSort (A,s)) and
A6: for s being SortSymbol of S1 holds W2 . s = meet (OSSubSort (A,s)) ; ::_thesis: W1 = W2
 for s being set st s in the carrier of S1 holds
W1 . s = W2 . s
proof
let s be set ; ::_thesis: ( s in the carrier of S1 implies W1 . s = W2 . s )
assume  s in the carrier of S1 ; ::_thesis: W1 . s = W2 . s
then reconsider s = s as SortSymbol of S1 ;
 W1 . s = meet (OSSubSort (A,s)) by A5;
hence  W1 . s = W2 . s by A6; ::_thesis: verum
end;
hence  W1 = W2 by PBOOLE:3; ::_thesis: verum
end;
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
proof
set x = the Element of OSSubSort OU0;
 the Element of OSSubSort OU0 in  {  y where y is Element of SubSort OU0 : y is OrderSortedSet of S1  }  ;
then consider x1 being Element of SubSort OU0 such that
 the Element of OSSubSort OU0 = x1 and
A1: x1 is OrderSortedSet of S1 ;
reconsider x2 = x1 as MSSubset of OU0 by MSUALG_2:def_11;
reconsider x3 = x2 as OSSubset of OU0 by A1, Def2;
take  x3 ; ::_thesis: x3 is opers_closed
thus  x3 is opers_closed by MSUALG_2:def_11; ::_thesis: verum
end;
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
proof
let S1 be OrderSortedSign; ::_thesis: for OU0 being OSAlgebra of S1
for A being OSSubset of OU0 holds (OSConstants OU0) \/ A c= OSMSubSort A
let OU0 be OSAlgebra of S1; ::_thesis: for A being OSSubset of OU0 holds (OSConstants OU0) \/ A c= OSMSubSort A
let A be OSSubset of OU0; ::_thesis: (OSConstants OU0) \/ A c= OSMSubSort A
let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in the carrier of S1 or ((OSConstants OU0) \/ A) . i c= (OSMSubSort A) . i )
assume  i in the carrier of S1 ; ::_thesis: ((OSConstants OU0) \/ A) . i c= (OSMSubSort A) . i
then reconsider s = i as SortSymbol of S1 ;
A1: for Z being set st Z in OSSubSort (A,s) holds
((OSConstants OU0) \/ A) . s c= Z
proof
let Z be set ; ::_thesis: ( Z in OSSubSort (A,s) implies ((OSConstants OU0) \/ A) . s c= Z )
assume  Z in OSSubSort (A,s) ; ::_thesis: ((OSConstants OU0) \/ A) . s c= Z
then consider B being OSSubset of OU0 such that
A2: B in OSSubSort A and
A3: Z = B . s by Def10;
 ( OSConstants OU0 c= B & A c= B ) by A2, Th19;
then  (OSConstants OU0) \/ A c= B by PBOOLE:16;
hence  ((OSConstants OU0) \/ A) . s c= Z by A3, PBOOLE:def_2; ::_thesis: verum
end;
 (OSMSubSort A) . s = meet (OSSubSort (A,s)) by Def11;
hence  ((OSConstants OU0) \/ A) . i c= (OSMSubSort A) . i by A1, SETFAM_1:5; ::_thesis: verum
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()
proof
let S1 be OrderSortedSign; ::_thesis: for OU0 being OSAlgebra of S1
for A being OSSubset of OU0 st (OSConstants OU0) \/ A is V8() holds
OSMSubSort A is V8()
let OU0 be OSAlgebra of S1; ::_thesis: for A being OSSubset of OU0 st (OSConstants OU0) \/ A is V8() holds
OSMSubSort A is V8()
let A be OSSubset of OU0; ::_thesis: ( (OSConstants OU0) \/ A is V8() implies OSMSubSort A is V8() )
assume A1: (OSConstants OU0) \/ A is V8() ; ::_thesis: OSMSubSort A is V8()
now__::_thesis:_for_i_being_set_st_i_in_the_carrier_of_S1_holds_
not_(OSMSubSort_A)_._i_is_empty
let i be set ; ::_thesis: ( i in the carrier of S1 implies not (OSMSubSort A) . i is empty )
assume  i in the carrier of S1 ; ::_thesis: not (OSMSubSort A) . i is empty
then reconsider s = i as SortSymbol of S1 ;
 for Z being set st Z in OSSubSort (A,s) holds
((OSConstants OU0) \/ A) . s c= Z
proof
let Z be set ; ::_thesis: ( Z in OSSubSort (A,s) implies ((OSConstants OU0) \/ A) . s c= Z )
assume  Z in OSSubSort (A,s) ; ::_thesis: ((OSConstants OU0) \/ A) . s c= Z
then consider B being OSSubset of OU0 such that
A2: B in OSSubSort A and
A3: Z = B . s by Def10;
 ( OSConstants OU0 c= B & A c= B ) by A2, Th19;
then  (OSConstants OU0) \/ A c= B by PBOOLE:16;
hence  ((OSConstants OU0) \/ A) . s c= Z by A3, PBOOLE:def_2; ::_thesis: verum
end;
then A4: ((OSConstants OU0) \/ A) . s c= meet (OSSubSort (A,s)) by SETFAM_1:5;
 ex x being set st x in ((OSConstants OU0) \/ A) . s by A1, XBOOLE_0:def_1;
hence  not (OSMSubSort A) . i is empty by A4, Def11; ::_thesis: verum
end;
hence  OSMSubSort A is V8() by PBOOLE:def_13; ::_thesis: verum
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
proof
let S1 be OrderSortedSign; ::_thesis: 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
let OU0 be OSAlgebra of S1; ::_thesis: 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
let o be OperSymbol of S1; ::_thesis: 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
let A, B be OSSubset of OU0; ::_thesis: ( B in OSSubSort A implies (((OSMSubSort A) #) * the Arity of S1) . o c= ((B #) * the Arity of S1) . o )
assume A1: B in OSSubSort A ; ::_thesis: (((OSMSubSort A) #) * the Arity of S1) . o c= ((B #) * the Arity of S1) . o
 OSMSubSort A c= B
proof
let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in the carrier of S1 or (OSMSubSort A) . i c= B . i )
assume  i in the carrier of S1 ; ::_thesis: (OSMSubSort A) . i c= B . i
then reconsider s = i as SortSymbol of S1 ;
 ( (OSMSubSort A) . s = meet (OSSubSort (A,s)) & B . s in OSSubSort (A,s) ) by A1, Def10, Def11;
hence  (OSMSubSort A) . i c= B . i by SETFAM_1:3; ::_thesis: verum
end;
hence  (((OSMSubSort A) #) * the Arity of S1) . o c= ((B #) * the Arity of S1) . o by MSUALG_2:2; ::_thesis: verum
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
proof
let S1 be OrderSortedSign; ::_thesis: 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
let OU0 be OSAlgebra of S1; ::_thesis: 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
let o be OperSymbol of S1; ::_thesis: 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
let A, B be OSSubset of OU0; ::_thesis: ( B in OSSubSort A implies rng ((Den (o,OU0)) | ((((OSMSubSort A) #) * the Arity of S1) . o)) c= (B * the ResultSort of S1) . o )
set m = (((OSMSubSort A) #) * the Arity of S1) . o;
set b = ((B #) * the Arity of S1) . o;
set d = Den (o,OU0);
assume A1: B in OSSubSort A ; ::_thesis: rng ((Den (o,OU0)) | ((((OSMSubSort A) #) * the Arity of S1) . o)) c= (B * the ResultSort of S1) . o
then  B is opers_closed by Th19;
then  B is_closed_on o by MSUALG_2:def_6;
then A2: rng ((Den (o,OU0)) | (((B #) * the Arity of S1) . o)) c= (B * the ResultSort of S1) . o by MSUALG_2:def_5;
 (((B #) * the Arity of S1) . o) /\ ((((OSMSubSort A) #) * the Arity of S1) . o) = (((OSMSubSort A) #) * the Arity of S1) . o by A1, Th26, XBOOLE_1:28;
then  (Den (o,OU0)) | ((((OSMSubSort A) #) * the Arity of S1) . o) = ((Den (o,OU0)) | (((B #) * the Arity of S1) . o)) | ((((OSMSubSort A) #) * the Arity of S1) . o) by RELAT_1:71;
then  rng ((Den (o,OU0)) | ((((OSMSubSort A) #) * the Arity of S1) . o)) c= rng ((Den (o,OU0)) | (((B #) * the Arity of S1) . o)) by RELAT_1:70;
hence  rng ((Den (o,OU0)) | ((((OSMSubSort A) #) * the Arity of S1) . o)) c= (B * the ResultSort of S1) . o by A2, XBOOLE_1:1; ::_thesis: verum
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
proof
let S1 be OrderSortedSign; ::_thesis: 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
let OU0 be OSAlgebra of S1; ::_thesis: 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
let o be OperSymbol of S1; ::_thesis: 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
let A be OSSubset of OU0; ::_thesis: rng ((Den (o,OU0)) | ((((OSMSubSort A) #) * the Arity of S1) . o)) c= ((OSMSubSort A) * the ResultSort of S1) . o
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng ((Den (o,OU0)) | ((((OSMSubSort A) #) * the Arity of S1) . o)) or x in ((OSMSubSort A) * the ResultSort of S1) . o )
assume that
A1: x in rng ((Den (o,OU0)) | ((((OSMSubSort A) #) * the Arity of S1) . o)) and
A2: not x in ((OSMSubSort A) * the ResultSort of S1) . o ; ::_thesis: contradiction
set r = the_result_sort_of o;
A3: ( the_result_sort_of o = the ResultSort of S1 . o & dom the ResultSort of S1 = the carrier' of S1 ) by FUNCT_2:def_1, MSUALG_1:def_2;
then ((OSMSubSort A) * the ResultSort of S1) . o = (OSMSubSort A) . (the_result_sort_of o) by FUNCT_1:13
.= meet (OSSubSort (A,(the_result_sort_of o))) by Def11 ;
then consider X being set  such that
A4: X in OSSubSort (A,(the_result_sort_of o)) and
A5: not x in X by A2, SETFAM_1:def_1;
consider B being OSSubset of OU0 such that
A6: B in OSSubSort A and
A7: B . (the_result_sort_of o) = X by A4, Def10;
 rng ((Den (o,OU0)) | ((((OSMSubSort A) #) * the Arity of S1) . o)) c= (B * the ResultSort of S1) . o by A6, Th27;
then  x in (B * the ResultSort of S1) . o by A1;
hence  contradiction by A3, A5, A7, FUNCT_1:13; ::_thesis: verum
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 )
proof
let S1 be OrderSortedSign; ::_thesis: for OU0 being OSAlgebra of S1
for A being OSSubset of OU0 holds
( OSMSubSort A is opers_closed & A c= OSMSubSort A )
let OU0 be OSAlgebra of S1; ::_thesis: for A being OSSubset of OU0 holds
( OSMSubSort A is opers_closed & A c= OSMSubSort A )
let A be OSSubset of OU0; ::_thesis: ( OSMSubSort A is opers_closed & A c= OSMSubSort A )
thus  OSMSubSort A is opers_closed ::_thesis: A c= OSMSubSort A
proof
let o1 be Element of the carrier' of S1; :: according to MSUALG_2:def_6 ::_thesis: OSMSubSort A is_closed_on o1
reconsider o = o1 as OperSymbol of S1 ;
 rng ((Den (o,OU0)) | ((((OSMSubSort A) #) * the Arity of S1) . o)) c= ((OSMSubSort A) * the ResultSort of S1) . o by Th28;
hence  OSMSubSort A is_closed_on o1 by MSUALG_2:def_5; ::_thesis: verum
end;
 ( A c= (OSConstants OU0) \/ A & (OSConstants OU0) \/ A c= OSMSubSort A ) by Th24, PBOOLE:14;
hence  A c= OSMSubSort A by PBOOLE:13; ::_thesis: verum
end;

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
proof
set M = MSAlgebra(# A,(Opers (OU0,A)) #);
 ( OU0 | A = MSAlgebra(# A,(Opers (OU0,A)) #) & A is OrderSortedSet of S1 ) by Def2, MSUALG_2:def_15;
hence  OU0 | A is order-sorted by OSALG_1:17; ::_thesis: verum
end;
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
proof
reconsider M1 = the Sorts of OU1, M2 = the Sorts of OU2 as OrderSortedSet of S1 by OSALG_1:17;
 M1 /\ M2 is OrderSortedSet of S1 by Th1;
then  the Sorts of (OU1 /\ OU2) is OrderSortedSet of S1 by MSUALG_2:def_16;
hence  OU1 /\ OU2 is order-sorted by OSALG_1:17; ::_thesis: verum
end;
end;

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 & ( 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 & ( for OU1 being OSSubAlgebra of OU0 st A is OSSubset of OU1 holds
b1 is OSSubAlgebra of OU1 ) )
proof
set a = OSMSubSort A;
reconsider u1 = OU0 | (OSMSubSort A) as strict OSSubAlgebra of OU0 ;
take  u1 ; ::_thesis: ( A is OSSubset of u1 & ( for OU1 being OSSubAlgebra of OU0 st A is OSSubset of OU1 holds
u1 is OSSubAlgebra of OU1 ) )
A1: u1 = MSAlgebra(# (OSMSubSort A),(Opers (OU0,(OSMSubSort A))) #) by MSUALG_2:def_15;
A2: A is OrderSortedSet of S1 by Def2;
 A c= OSMSubSort A by Th29;
then  A is MSSubset of u1 by A1, PBOOLE:def_18;
hence  A is OSSubset of u1 by A2, Def2; ::_thesis: for OU1 being OSSubAlgebra of OU0 st A is OSSubset of OU1 holds
u1 is OSSubAlgebra of OU1
let U2 be OSSubAlgebra of OU0; ::_thesis: ( A is OSSubset of U2 implies u1 is OSSubAlgebra of U2 )
reconsider B1 = the Sorts of U2 as MSSubset of OU0 by MSUALG_2:def_9;
 B1 is OrderSortedSet of S1 by OSALG_1:17;
then reconsider B = B1 as OSSubset of OU0 by Def2;
assume  A is OSSubset of U2 ; ::_thesis: u1 is OSSubAlgebra of U2
then A3: ( B is opers_closed & A c= B ) by MSUALG_2:def_9, PBOOLE:def_18;
 OSConstants OU0 is OSSubset of U2 by Th13;
then  OSConstants OU0 c= B by PBOOLE:def_18;
then A4: B in OSSubSort A by A3, Th19;
 the Sorts of u1 c= the Sorts of U2
proof
let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in the carrier of S1 or the Sorts of u1 . i c= the Sorts of U2 . i )
assume  i in the carrier of S1 ; ::_thesis: the Sorts of u1 . i c= the Sorts of U2 . i
then reconsider s = i as SortSymbol of S1 ;
 ( the Sorts of u1 . s = meet (OSSubSort (A,s)) & B . s in OSSubSort (A,s) ) by A1, A4, Def10, Def11;
hence  the Sorts of u1 . i c= the Sorts of U2 . i by SETFAM_1:3; ::_thesis: verum
end;
hence  u1 is OSSubAlgebra of U2 by MSUALG_2:8; ::_thesis: verum
end;
uniqueness
 for b1, b2 being strict OSSubAlgebra of OU0 st A is OSSubset of b1 & ( for OU1 being OSSubAlgebra of OU0 st A is OSSubset of OU1 holds
b1 is OSSubAlgebra of OU1 ) & A is OSSubset of b2 & ( for OU1 being OSSubAlgebra of OU0 st A is OSSubset of OU1 holds
b2 is OSSubAlgebra of OU1 ) holds
b1 = b2
proof
let W1, W2 be strict OSSubAlgebra of OU0; ::_thesis: ( A is OSSubset of W1 & ( for OU1 being OSSubAlgebra of OU0 st A is OSSubset of OU1 holds
W1 is OSSubAlgebra of OU1 ) & A is OSSubset of W2 & ( for OU1 being OSSubAlgebra of OU0 st A is OSSubset of OU1 holds
W2 is OSSubAlgebra of OU1 ) implies W1 = W2 )
assume  ( A is OSSubset of W1 & ( for U1 being OSSubAlgebra of OU0 st A is OSSubset of U1 holds
W1 is OSSubAlgebra of U1 ) & A is OSSubset of W2 & ( for U2 being OSSubAlgebra of OU0 st A is OSSubset of U2 holds
W2 is OSSubAlgebra of U2 ) ) ; ::_thesis: W1 = W2
then  ( W1 is strict OSSubAlgebra of W2 & W2 is strict OSSubAlgebra of W1 ) ;
hence  W1 = W2 by MSUALG_2:7; ::_thesis: verum
end;
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 & ( for OU1 being OSSubAlgebra of OU0 st A is OSSubset of OU1 holds
b4 is OSSubAlgebra of OU1 ) ) );

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 )
proof
let S1 be OrderSortedSign; ::_thesis: 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 )
let OU0 be OSAlgebra of S1; ::_thesis: for A being OSSubset of OU0 holds
( GenOSAlg A = OU0 | (OSMSubSort A) & the Sorts of (GenOSAlg A) = OSMSubSort A )
let A be OSSubset of OU0; ::_thesis: ( GenOSAlg A = OU0 | (OSMSubSort A) & the Sorts of (GenOSAlg A) = OSMSubSort A )
set a = OSMSubSort A;
reconsider u1 = OU0 | (OSMSubSort A) as strict OSSubAlgebra of OU0 ;
A1: u1 = MSAlgebra(# (OSMSubSort A),(Opers (OU0,(OSMSubSort A))) #) by MSUALG_2:def_15;
A2: A c= OSMSubSort A by Th29;
A3: A is OrderSortedSet of S1 by Def2;
A4: ( A is OSSubset of u1 & ( for OU1 being OSSubAlgebra of OU0 st A is OSSubset of OU1 holds
u1 is OSSubAlgebra of OU1 ) )
proof
 A is MSSubset of u1 by A2, A1, PBOOLE:def_18;
hence  A is OSSubset of u1 by A3, Def2; ::_thesis: for OU1 being OSSubAlgebra of OU0 st A is OSSubset of OU1 holds
u1 is OSSubAlgebra of OU1
let U2 be OSSubAlgebra of OU0; ::_thesis: ( A is OSSubset of U2 implies u1 is OSSubAlgebra of U2 )
reconsider B1 = the Sorts of U2 as MSSubset of OU0 by MSUALG_2:def_9;
 B1 is OrderSortedSet of S1 by OSALG_1:17;
then reconsider B = B1 as OSSubset of OU0 by Def2;
assume  A is OSSubset of U2 ; ::_thesis: u1 is OSSubAlgebra of U2
then A5: ( B is opers_closed & A c= B ) by MSUALG_2:def_9, PBOOLE:def_18;
 OSConstants OU0 is OSSubset of U2 by Th13;
then  OSConstants OU0 c= B by PBOOLE:def_18;
then A6: B in OSSubSort A by A5, Th19;
 the Sorts of u1 c= the Sorts of U2
proof
let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in the carrier of S1 or the Sorts of u1 . i c= the Sorts of U2 . i )
assume  i in the carrier of S1 ; ::_thesis: the Sorts of u1 . i c= the Sorts of U2 . i
then reconsider s = i as SortSymbol of S1 ;
 ( the Sorts of u1 . s = meet (OSSubSort (A,s)) & B . s in OSSubSort (A,s) ) by A1, A6, Def10, Def11;
hence  the Sorts of u1 . i c= the Sorts of U2 . i by SETFAM_1:3; ::_thesis: verum
end;
hence  u1 is OSSubAlgebra of U2 by MSUALG_2:8; ::_thesis: verum
end;
hence  GenOSAlg A = OU0 | (OSMSubSort A) by Def12; ::_thesis: the Sorts of (GenOSAlg A) = OSMSubSort A
thus  the Sorts of (GenOSAlg A) = OSMSubSort A by A1, A4, Def12; ::_thesis: verum
end;

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 )
proof
let S be non empty non void ManySortedSign ; ::_thesis: 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 )
let U0 be MSAlgebra over S; ::_thesis: for A being MSSubset of U0 holds
( GenMSAlg A = U0 | (MSSubSort A) & the Sorts of (GenMSAlg A) = MSSubSort A )
let A be MSSubset of U0; ::_thesis: ( GenMSAlg A = U0 | (MSSubSort A) & the Sorts of (GenMSAlg A) = MSSubSort A )
set a = MSSubSort A;
reconsider u1 = U0 | (MSSubSort A) as strict MSSubAlgebra of U0 ;
A1: u1 = MSAlgebra(# (MSSubSort A),(Opers (U0,(MSSubSort A))) #) by MSUALG_2:20, MSUALG_2:def_15;
A2: A c= MSSubSort A by MSUALG_2:20;
A3: ( A is MSSubset of u1 & ( for U1 being MSSubAlgebra of U0 st A is MSSubset of U1 holds
u1 is MSSubAlgebra of U1 ) )
proof
thus  A is MSSubset of u1 by A2, A1, PBOOLE:def_18; ::_thesis: for U1 being MSSubAlgebra of U0 st A is MSSubset of U1 holds
u1 is MSSubAlgebra of U1
let U2 be MSSubAlgebra of U0; ::_thesis: ( A is MSSubset of U2 implies u1 is MSSubAlgebra of U2 )
reconsider B = the Sorts of U2 as MSSubset of U0 by MSUALG_2:def_9;
 Constants U0 is MSSubset of U2 by MSUALG_2:10;
then A4: Constants U0 c= B by PBOOLE:def_18;
assume  A is MSSubset of U2 ; ::_thesis: u1 is MSSubAlgebra of U2
then  ( B is opers_closed & A c= B ) by MSUALG_2:def_9, PBOOLE:def_18;
then A5: B in SubSort A by A4, MSUALG_2:13;
 the Sorts of u1 c= the Sorts of U2
proof
let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in the carrier of S or the Sorts of u1 . i c= the Sorts of U2 . i )
assume  i in the carrier of S ; ::_thesis: the Sorts of u1 . i c= the Sorts of U2 . i
then reconsider s = i as SortSymbol of S ;
 ( the Sorts of u1 . s = meet (SubSort (A,s)) & B . s in SubSort (A,s) ) by A1, A5, MSUALG_2:def_13, MSUALG_2:def_14;
hence  the Sorts of u1 . i c= the Sorts of U2 . i by SETFAM_1:3; ::_thesis: verum
end;
hence  u1 is MSSubAlgebra of U2 by MSUALG_2:8; ::_thesis: verum
end;
hence  GenMSAlg A = U0 | (MSSubSort A) by MSUALG_2:def_17; ::_thesis: the Sorts of (GenMSAlg A) = MSSubSort A
thus  the Sorts of (GenMSAlg A) = MSSubSort A by A1, A3, MSUALG_2:def_17; ::_thesis: verum
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)
proof
let S1 be OrderSortedSign; ::_thesis: for OU0 being OSAlgebra of S1
for A being OSSubset of OU0 holds the Sorts of (GenMSAlg A) c= the Sorts of (GenOSAlg A)
let OU0 be OSAlgebra of S1; ::_thesis: for A being OSSubset of OU0 holds the Sorts of (GenMSAlg A) c= the Sorts of (GenOSAlg A)
let A be OSSubset of OU0; ::_thesis: the Sorts of (GenMSAlg A) c= the Sorts of (GenOSAlg A)
set GM = GenMSAlg A;
set GO = GenOSAlg A;
let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in the carrier of S1 or the Sorts of (GenMSAlg A) . i c= the Sorts of (GenOSAlg A) . i )
assume  i in the carrier of S1 ; ::_thesis: the Sorts of (GenMSAlg A) . i c= the Sorts of (GenOSAlg A) . i
then reconsider s = i as SortSymbol of S1 ;
 the Sorts of (GenMSAlg A) = MSSubSort A by Th31;
then A1: the Sorts of (GenMSAlg A) . s = meet (SubSort (A,s)) by MSUALG_2:def_14;
 the Sorts of (GenOSAlg A) = OSMSubSort A by Th30;
then  the Sorts of (GenOSAlg A) . s = meet (OSSubSort (A,s)) by Def11;
hence  the Sorts of (GenMSAlg A) . i c= the Sorts of (GenOSAlg A) . i by A1, Th22, SETFAM_1:6; ::_thesis: verum
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;

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
proof
let S1 be OrderSortedSign; ::_thesis: for OU0 being strict OSAlgebra of S1
for B being OSSubset of OU0 st B = the Sorts of OU0 holds
GenOSAlg B = OU0
let OU0 be strict OSAlgebra of S1; ::_thesis: for B being OSSubset of OU0 st B = the Sorts of OU0 holds
GenOSAlg B = OU0
let B be OSSubset of OU0; ::_thesis: ( B = the Sorts of OU0 implies GenOSAlg B = OU0 )
assume  B = the Sorts of OU0 ; ::_thesis: GenOSAlg B = OU0
then A1: GenMSAlg B = OU0 by MSUALG_2:21;
 GenMSAlg B is strict MSSubAlgebra of GenOSAlg B by Th32, MSUALG_2:8;
hence  GenOSAlg B = OU0 by A1, MSUALG_2:7; ::_thesis: verum
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
proof
let S1 be OrderSortedSign; ::_thesis: 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
let OU0 be OSAlgebra of S1; ::_thesis: for OU1 being strict OSSubAlgebra of OU0
for B being OSSubset of OU0 st B = the Sorts of OU1 holds
GenOSAlg B = OU1
let OU1 be strict OSSubAlgebra of OU0; ::_thesis: for B being OSSubset of OU0 st B = the Sorts of OU1 holds
GenOSAlg B = OU1
let B be OSSubset of OU0; ::_thesis: ( B = the Sorts of OU1 implies GenOSAlg B = OU1 )
set W = GenOSAlg B;
assume A1: B = the Sorts of OU1 ; ::_thesis: GenOSAlg B = OU1
then A2: B is MSSubset of OU1 by PBOOLE:def_18;
 B is OSSubset of GenOSAlg B by Def12;
then  the Sorts of OU1 c= the Sorts of (GenOSAlg B) by A1, PBOOLE:def_18;
then A3: OU1 is strict MSSubAlgebra of GenOSAlg B by MSUALG_2:8;
 B is OrderSortedSet of S1 by Def2;
then  B is OSSubset of OU1 by A2, Def2;
then  GenOSAlg B is strict OSSubAlgebra of OU1 by Def12;
hence  GenOSAlg B = OU1 by A3, MSUALG_2:7; ::_thesis: verum
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)
proof
let S1 be OrderSortedSign; ::_thesis: for U0 being non-empty OSAlgebra of S1
for U1 being OSSubAlgebra of U0 holds (GenOSAlg (OSConstants U0)) /\ U1 = GenOSAlg (OSConstants U0)
let U0 be non-empty OSAlgebra of S1; ::_thesis: for U1 being OSSubAlgebra of U0 holds (GenOSAlg (OSConstants U0)) /\ U1 = GenOSAlg (OSConstants U0)
let U1 be OSSubAlgebra of U0; ::_thesis: (GenOSAlg (OSConstants U0)) /\ U1 = GenOSAlg (OSConstants U0)
set C = OSConstants U0;
set G = GenOSAlg (OSConstants U0);
 OSConstants U0 is OSSubset of U1 by Th13;
then  GenOSAlg (OSConstants U0) is strict OSSubAlgebra of U1 by Def12;
then  the Sorts of (GenOSAlg (OSConstants U0)) is MSSubset of U1 by MSUALG_2:def_9;
then  ( the Sorts of ((GenOSAlg (OSConstants U0)) /\ U1) = the Sorts of (GenOSAlg (OSConstants U0)) /\ the Sorts of U1 & the Sorts of (GenOSAlg (OSConstants U0)) c= the Sorts of U1 ) by MSUALG_2:def_16, PBOOLE:def_18;
then  the Sorts of ((GenOSAlg (OSConstants U0)) /\ U1) = the Sorts of (GenOSAlg (OSConstants U0)) by PBOOLE:23;
hence  (GenOSAlg (OSConstants U0)) /\ U1 = GenOSAlg (OSConstants U0) by MSUALG_2:9; ::_thesis: verum
end;

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
proof
set B = the Sorts of U1 \/ the Sorts of U2;
 the Sorts of U2 is MSSubset of U0 by MSUALG_2:def_9;
then A1: the Sorts of U2 c= the Sorts of U0 by PBOOLE:def_18;
 the Sorts of U1 is MSSubset of U0 by MSUALG_2:def_9;
then  the Sorts of U1 c= the Sorts of U0 by PBOOLE:def_18;
then  the Sorts of U1 \/ the Sorts of U2 c= the Sorts of U0 by A1, PBOOLE:16;
then reconsider B = the Sorts of U1 \/ the Sorts of U2 as MSSubset of U0 by PBOOLE:def_18;
reconsider B1 = the Sorts of U1, B2 = the Sorts of U2 as OrderSortedSet of S1 by OSALG_1:17;
 B = B1 \/ B2 ;
then  B is OrderSortedSet of S1 by Th2;
then reconsider B0 = B as OSSubset of U0 by Def2;
take  GenOSAlg B0 ; ::_thesis: for A being OSSubset of U0 st A = the Sorts of U1 \/ the Sorts of U2 holds
GenOSAlg B0 = GenOSAlg A
thus  for A being OSSubset of U0 st A = the Sorts of U1 \/ the Sorts of U2 holds
GenOSAlg B0 = GenOSAlg A ; ::_thesis: verum
end;
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 ) & ( for A being OSSubset of U0 st A = the Sorts of U1 \/ the Sorts of U2 holds
b2 = GenOSAlg A ) holds
b1 = b2
proof
reconsider B1 = the Sorts of U1, B2 = the Sorts of U2 as OrderSortedSet of S1 by OSALG_1:17;
set B = the Sorts of U1 \/ the Sorts of U2;
 the Sorts of U2 is MSSubset of U0 by MSUALG_2:def_9;
then A2: the Sorts of U2 c= the Sorts of U0 by PBOOLE:def_18;
 the Sorts of U1 is MSSubset of U0 by MSUALG_2:def_9;
then  the Sorts of U1 c= the Sorts of U0 by PBOOLE:def_18;
then  the Sorts of U1 \/ the Sorts of U2 c= the Sorts of U0 by A2, PBOOLE:16;
then reconsider B = the Sorts of U1 \/ the Sorts of U2 as MSSubset of U0 by PBOOLE:def_18;
let W1, W2 be strict OSSubAlgebra of U0; ::_thesis: ( ( for A being OSSubset of U0 st A = the Sorts of U1 \/ the Sorts of U2 holds
W1 = GenOSAlg A ) & ( for A being OSSubset of U0 st A = the Sorts of U1 \/ the Sorts of U2 holds
W2 = GenOSAlg A ) implies W1 = W2 )
assume that
A3: for A being OSSubset of U0 st A = the Sorts of U1 \/ the Sorts of U2 holds
W1 = GenOSAlg A and
A4: for A being OSSubset of U0 st A = the Sorts of U1 \/ the Sorts of U2 holds
W2 = GenOSAlg A ; ::_thesis: W1 = W2
 B = B1 \/ B2 ;
then  B is OrderSortedSet of S1 by Th2;
then reconsider B0 = B as OSSubset of U0 by Def2;
 W1 = GenOSAlg B0 by A3;
hence  W1 = W2 by A4; ::_thesis: verum
end;
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
proof
let S1 be OrderSortedSign; ::_thesis: 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
let U0 be non-empty OSAlgebra of S1; ::_thesis: 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
let U1 be OSSubAlgebra of U0; ::_thesis: for A, B being OSSubset of U0 st B = A \/ the Sorts of U1 holds
(GenOSAlg A) "\/"_os U1 = GenOSAlg B
let A, B be OSSubset of U0; ::_thesis: ( B = A \/ the Sorts of U1 implies (GenOSAlg A) "\/"_os U1 = GenOSAlg B )
assume A1: B = A \/ the Sorts of U1 ; ::_thesis: (GenOSAlg A) "\/"_os U1 = GenOSAlg B
reconsider u1m = the Sorts of U1, am = the Sorts of (GenOSAlg A) as MSSubset of U0 by MSUALG_2:def_9;
A2: ( the Sorts of U1 is OrderSortedSet of S1 & the Sorts of (GenOSAlg A) is OrderSortedSet of S1 ) by OSALG_1:17;
then reconsider u1 = u1m, a = am as OSSubset of U0 by Def2;
 ( a c= the Sorts of U0 & u1 c= the Sorts of U0 ) by PBOOLE:def_18;
then  a \/ u1 c= the Sorts of U0 by PBOOLE:16;
then reconsider b = a \/ u1 as MSSubset of U0 by PBOOLE:def_18;
A3: a \/ u1 is OrderSortedSet of S1 by A2, Th2;
then reconsider b = b as OSSubset of U0 by Def2;
A4: (GenOSAlg A) "\/"_os U1 = GenOSAlg b by Def13;
then  a \/ u1 is OSSubset of (GenOSAlg A) "\/"_os U1 by Def12;
then A5: a \/ u1 c= the Sorts of ((GenOSAlg A) "\/"_os U1) by PBOOLE:def_18;
 A is OSSubset of GenOSAlg A by Def12;
then A6: A c= the Sorts of (GenOSAlg A) by PBOOLE:def_18;
then  A \/ u1 c= a \/ u1 by PBOOLE:20;
then  B c= the Sorts of ((GenOSAlg A) "\/"_os U1) by A1, A5, PBOOLE:13;
then A7: B is MSSubset of ((GenOSAlg A) "\/"_os U1) by PBOOLE:def_18;
A8: A is OrderSortedSet of S1 by Def2;
A9: the Sorts of ((GenOSAlg A) /\ (GenOSAlg B)) = the Sorts of (GenOSAlg A) /\ the Sorts of (GenOSAlg B) by MSUALG_2:def_16;
 B is OSSubset of GenOSAlg B by Def12;
then A10: B c= the Sorts of (GenOSAlg B) by PBOOLE:def_18;
 A c= B by A1, PBOOLE:14;
then  A c= the Sorts of (GenOSAlg B) by A10, PBOOLE:13;
then  A c= the Sorts of (GenOSAlg A) /\ the Sorts of (GenOSAlg B) by A6, PBOOLE:17;
then  A is MSSubset of ((GenOSAlg A) /\ (GenOSAlg B)) by A9, PBOOLE:def_18;
then  A is OSSubset of (GenOSAlg A) /\ (GenOSAlg B) by A8, Def2;
then  GenOSAlg A is OSSubAlgebra of (GenOSAlg A) /\ (GenOSAlg B) by Def12;
then  a is MSSubset of ((GenOSAlg A) /\ (GenOSAlg B)) by MSUALG_2:def_9;
then A11: a c= the Sorts of (GenOSAlg A) /\ the Sorts of (GenOSAlg B) by A9, PBOOLE:def_18;
 the Sorts of (GenOSAlg A) /\ the Sorts of (GenOSAlg B) c= a by PBOOLE:15;
then  a = the Sorts of (GenOSAlg A) /\ the Sorts of (GenOSAlg B) by A11, PBOOLE:146;
then A12: a c= the Sorts of (GenOSAlg B) by PBOOLE:15;
 u1 c= B by A1, PBOOLE:14;
then  u1 c= the Sorts of (GenOSAlg B) by A10, PBOOLE:13;
then  b c= the Sorts of (GenOSAlg B) by A12, PBOOLE:16;
then  b is MSSubset of (GenOSAlg B) by PBOOLE:def_18;
then  b is OSSubset of GenOSAlg B by A3, Def2;
then A13: GenOSAlg b is strict OSSubAlgebra of GenOSAlg B by Def12;
 B is OrderSortedSet of S1 by Def2;
then  B is OSSubset of (GenOSAlg A) "\/"_os U1 by A7, Def2;
then  GenOSAlg B is strict OSSubAlgebra of (GenOSAlg A) "\/"_os U1 by Def12;
hence  (GenOSAlg A) "\/"_os U1 = GenOSAlg B by A4, A13, MSUALG_2:7; ::_thesis: verum
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
proof
let S1 be OrderSortedSign; ::_thesis: 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
let U0 be non-empty OSAlgebra of S1; ::_thesis: 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
let U1 be OSSubAlgebra of U0; ::_thesis: for B being OSSubset of U0 st B = the Sorts of U0 holds
(GenOSAlg B) "\/"_os U1 = GenOSAlg B
let B be OSSubset of U0; ::_thesis: ( B = the Sorts of U0 implies (GenOSAlg B) "\/"_os U1 = GenOSAlg B )
A1: the Sorts of U1 is MSSubset of U0 by MSUALG_2:def_9;
assume  B = the Sorts of U0 ; ::_thesis: (GenOSAlg B) "\/"_os U1 = GenOSAlg B
then  the Sorts of U1 c= B by A1, PBOOLE:def_18;
then  B \/ the Sorts of U1 = B by PBOOLE:22;
hence  (GenOSAlg B) "\/"_os U1 = GenOSAlg B by Th37; ::_thesis: verum
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
proof
let S1 be OrderSortedSign; ::_thesis: for U0 being non-empty OSAlgebra of S1
for U1, U2 being OSSubAlgebra of U0 holds U1 "\/"_os U2 = U2 "\/"_os U1
let U0 be non-empty OSAlgebra of S1; ::_thesis: for U1, U2 being OSSubAlgebra of U0 holds U1 "\/"_os U2 = U2 "\/"_os U1
let U1, U2 be OSSubAlgebra of U0; ::_thesis: U1 "\/"_os U2 = U2 "\/"_os U1
reconsider u1 = the Sorts of U1, u2 = the Sorts of U2 as MSSubset of U0 by MSUALG_2:def_9;
 ( u1 c= the Sorts of U0 & u2 c= the Sorts of U0 ) by PBOOLE:def_18;
then  u1 \/ u2 c= the Sorts of U0 by PBOOLE:16;
then reconsider A1 = u1 \/ u2 as MSSubset of U0 by PBOOLE:def_18;
 ( u1 is OrderSortedSet of S1 & u2 is OrderSortedSet of S1 ) by OSALG_1:17;
then  A1 is OrderSortedSet of S1 by Th2;
then reconsider A = A1 as OSSubset of U0 by Def2;
 U1 "\/"_os U2 = GenOSAlg A by Def13;
hence  U1 "\/"_os U2 = U2 "\/"_os U1 by Def13; ::_thesis: verum
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
proof
let S1 be OrderSortedSign; ::_thesis: for U0 being non-empty OSAlgebra of S1
for U1, U2 being strict OSSubAlgebra of U0 holds U1 /\ (U1 "\/"_os U2) = U1
let U0 be non-empty OSAlgebra of S1; ::_thesis: for U1, U2 being strict OSSubAlgebra of U0 holds U1 /\ (U1 "\/"_os U2) = U1
let U1, U2 be strict OSSubAlgebra of U0; ::_thesis: U1 /\ (U1 "\/"_os U2) = U1
reconsider u1 = the Sorts of U1, u2 = the Sorts of U2 as MSSubset of U0 by MSUALG_2:def_9;
reconsider u112 = the Sorts of (U1 /\ (U1 "\/"_os U2)) as MSSubset of U0 by MSUALG_2:def_9;
A1: the Charact of (U1 /\ (U1 "\/"_os U2)) = Opers (U0,u112) by MSUALG_2:def_16;
 ( u1 c= the Sorts of U0 & u2 c= the Sorts of U0 ) by PBOOLE:def_18;
then  u1 \/ u2 c= the Sorts of U0 by PBOOLE:16;
then reconsider A = u1 \/ u2 as MSSubset of U0 by PBOOLE:def_18;
 ( u1 is OrderSortedSet of S1 & u2 is OrderSortedSet of S1 ) by OSALG_1:17;
then  A is OrderSortedSet of S1 by Th2;
then reconsider A = A as OSSubset of U0 by Def2;
A2: the Sorts of (U1 /\ (U1 "\/"_os U2)) = the Sorts of U1 /\ the Sorts of (U1 "\/"_os U2) by MSUALG_2:def_16;
 U1 "\/"_os U2 = GenOSAlg A by Def13;
then  A is OSSubset of U1 "\/"_os U2 by Def12;
then A3: A c= the Sorts of (U1 "\/"_os U2) by PBOOLE:def_18;
 the Sorts of U1 c= A by PBOOLE:14;
then  the Sorts of U1 c= the Sorts of (U1 "\/"_os U2) by A3, PBOOLE:13;
then A4: the Sorts of U1 c= the Sorts of (U1 /\ (U1 "\/"_os U2)) by A2, PBOOLE:17;
 the Sorts of (U1 /\ (U1 "\/"_os U2)) c= the Sorts of U1 by A2, PBOOLE:15;
then  the Sorts of (U1 /\ (U1 "\/"_os U2)) = the Sorts of U1 by A4, PBOOLE:146;
hence  U1 /\ (U1 "\/"_os U2) = U1 by A1, MSUALG_2:def_9; ::_thesis: verum
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
proof
let S1 be OrderSortedSign; ::_thesis: for U0 being non-empty OSAlgebra of S1
for U1, U2 being strict OSSubAlgebra of U0 holds (U1 /\ U2) "\/"_os U2 = U2
let U0 be non-empty OSAlgebra of S1; ::_thesis: for U1, U2 being strict OSSubAlgebra of U0 holds (U1 /\ U2) "\/"_os U2 = U2
let U1, U2 be strict OSSubAlgebra of U0; ::_thesis: (U1 /\ U2) "\/"_os U2 = U2
reconsider u12 = the Sorts of (U1 /\ U2), u2 = the Sorts of U2 as MSSubset of U0 by MSUALG_2:def_9;
A1: ( u12 is OrderSortedSet of S1 & u2 is OrderSortedSet of S1 ) by OSALG_1:17;
then reconsider u12 = u12, u2 = u2 as OSSubset of U0 by Def2;
 ( u12 c= the Sorts of U0 & u2 c= the Sorts of U0 ) by PBOOLE:def_18;
then  u12 \/ u2 c= the Sorts of U0 by PBOOLE:16;
then reconsider A = u12 \/ u2 as MSSubset of U0 by PBOOLE:def_18;
 A is OrderSortedSet of S1 by A1, Th2;
then reconsider A = u12 \/ u2 as OSSubset of U0 by Def2;
 u12 = the Sorts of U1 /\ the Sorts of U2 by MSUALG_2:def_16;
then  u12 c= u2 by PBOOLE:15;
then A2: A = u2 by PBOOLE:22;
 (U1 /\ U2) "\/"_os U2 = GenOSAlg A by Def13;
hence  (U1 /\ U2) "\/"_os U2 = U2 by A2, Th35; ::_thesis: verum
end;

begin

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 )
proof
set X =  {  (GenOSAlg (@ A)) where A is Element of OSSubSort OU0 : verum  }  ;
take   {  (GenOSAlg (@ A)) where A is Element of OSSubSort OU0 : verum  }  ; ::_thesis: for x being set holds
( x in  {  (GenOSAlg (@ A)) where A is Element of OSSubSort OU0 : verum  }  iff x is strict OSSubAlgebra of OU0 )
let x be set ; ::_thesis: ( x in  {  (GenOSAlg (@ A)) where A is Element of OSSubSort OU0 : verum  }  iff x is strict OSSubAlgebra of OU0 )
thus  ( x in  {  (GenOSAlg (@ A)) where A is Element of OSSubSort OU0 : verum  }  implies x is strict OSSubAlgebra of OU0 ) ::_thesis: ( x is strict OSSubAlgebra of OU0 implies x in  {  (GenOSAlg (@ A)) where A is Element of OSSubSort OU0 : verum  }  )
proof
assume  x in  {  (GenOSAlg (@ A)) where A is Element of OSSubSort OU0 : verum  }  ; ::_thesis: x is strict OSSubAlgebra of OU0
then  ex A being Element of OSSubSort OU0 st x = GenOSAlg (@ A) ;
hence  x is strict OSSubAlgebra of OU0 ; ::_thesis: verum
end;
assume  x is strict OSSubAlgebra of OU0 ; ::_thesis: x in  {  (GenOSAlg (@ A)) where A is Element of OSSubSort OU0 : verum  }
then reconsider a = x as strict OSSubAlgebra of OU0 ;
reconsider A = the Sorts of a as OSSubset of OU0 by Th5;
 A is opers_closed by Th5;
then reconsider h = A as Element of OSSubSort OU0 by Th20;
 a = GenOSAlg (@ h) by Th35;
hence  x in  {  (GenOSAlg (@ A)) where A is Element of OSSubSort OU0 : verum  }  ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being set st ( for x being set holds
( x in b1 iff x is strict OSSubAlgebra of OU0 ) ) & ( for x being set holds
( x in b2 iff x is strict OSSubAlgebra of OU0 ) ) holds
b1 = b2
proof
defpred S1[ set ] means $1 is strict OSSubAlgebra of OU0;
thus  for X1, X2 being set st ( for x being set holds
( x in X1 iff S1[x] ) ) & ( for x being set holds
( x in X2 iff S1[x] ) ) holds
X1 = X2 from XBOOLE_0:sch_3(); ::_thesis: verum
end;
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
proof
let S1 be OrderSortedSign; ::_thesis: for OU0 being OSAlgebra of S1 holds OSSub OU0 c= MSSub OU0
let OU0 be OSAlgebra of S1; ::_thesis: OSSub OU0 c= MSSub OU0
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in OSSub OU0 or x in MSSub OU0 )
assume  x in OSSub OU0 ; ::_thesis: x in MSSub OU0
then  x is strict MSSubAlgebra of OU0 by Def14;
hence  x in MSSub OU0 by MSUALG_2:def_19; ::_thesis: verum
end;

registration
let S be OrderSortedSign;
let U0 be OSAlgebra of S;
cluster OSSub U0 ->  non empty ;
coherence
 not OSSub U0 is empty
proof
set x = the strict OSSubAlgebra of U0;
 the strict OSSubAlgebra of U0 in OSSub U0 by Def14;
hence  not OSSub U0 is empty ; ::_thesis: verum
end;
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;

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 & 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 & y = U2 holds
b1 . (x,y) = U1 "\/"_os U2
proof
defpred S1[ Element of OSSub U0, Element of OSSub U0, set ] means  for U1, U2 being strict OSSubAlgebra of U0 st $1 = U1 & $2 = U2 holds
$3 = U1 "\/"_os U2;
A1: for x, y being Element of OSSub U0 ex z being Element of OSSub U0 st S1[x,y,z]
proof
let x, y be Element of OSSub U0; ::_thesis: ex z being Element of OSSub U0 st S1[x,y,z]
reconsider U1 = x, U2 = y as strict OSSubAlgebra of U0 by Def14;
reconsider z = U1 "\/"_os U2 as Element of OSSub U0 by Def14;
take  z ; ::_thesis: S1[x,y,z]
thus  S1[x,y,z] ; ::_thesis: verum
end;
consider o being BinOp of (OSSub U0) such that
A2: for a, b being Element of OSSub U0 holds S1[a,b,o . (a,b)] from BINOP_1:sch_3(A1);
take  o ; ::_thesis: for x, y being Element of OSSub U0
for U1, U2 being strict OSSubAlgebra of U0 st x = U1 & y = U2 holds
o . (x,y) = U1 "\/"_os U2
thus  for x, y being Element of OSSub U0
for U1, U2 being strict OSSubAlgebra of U0 st x = U1 & y = U2 holds
o . (x,y) = U1 "\/"_os U2 by A2; ::_thesis: verum
end;
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 & y = U2 holds
b1 . (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
b2 . (x,y) = U1 "\/"_os U2 ) holds
b1 = b2
proof
let o1, o2 be BinOp of (OSSub U0); ::_thesis: ( ( for x, y being Element of OSSub U0
for U1, U2 being strict OSSubAlgebra of U0 st x = U1 & y = U2 holds
o1 . (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
o2 . (x,y) = U1 "\/"_os U2 ) implies o1 = o2 )
assume that
A3: for x, y being Element of OSSub U0
for U1, U2 being strict OSSubAlgebra of U0 st x = U1 & y = U2 holds
o1 . (x,y) = U1 "\/"_os U2 and
A4: for x, y being Element of OSSub U0
for U1, U2 being strict OSSubAlgebra of U0 st x = U1 & y = U2 holds
o2 . (x,y) = U1 "\/"_os U2 ; ::_thesis: o1 = o2
 for x, y being Element of OSSub U0 holds o1 . (x,y) = o2 . (x,y)
proof
let x, y be Element of OSSub U0; ::_thesis: o1 . (x,y) = o2 . (x,y)
reconsider U1 = x, U2 = y as strict OSSubAlgebra of U0 by Def14;
 o1 . (x,y) = U1 "\/"_os U2 by A3;
hence  o1 . (x,y) = o2 . (x,y) by A4; ::_thesis: verum
end;
hence  o1 = o2 by BINOP_1:2; ::_thesis: verum
end;
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 & 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 & 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 & y = U2 holds
b1 . (x,y) = U1 /\ U2
proof
defpred S1[ Element of OSSub U0, Element of OSSub U0, set ] means  for U1, U2 being strict OSSubAlgebra of U0 st $1 = U1 & $2 = U2 holds
$3 = U1 /\ U2;
A1: for x, y being Element of OSSub U0 ex z being Element of OSSub U0 st S1[x,y,z]
proof
let x, y be Element of OSSub U0; ::_thesis: ex z being Element of OSSub U0 st S1[x,y,z]
reconsider U1 = x, U2 = y as strict OSSubAlgebra of U0 by Def14;
reconsider z = U1 /\ U2 as Element of OSSub U0 by Def14;
take  z ; ::_thesis: S1[x,y,z]
thus  S1[x,y,z] ; ::_thesis: verum
end;
consider o being BinOp of (OSSub U0) such that
A2: for a, b being Element of OSSub U0 holds S1[a,b,o . (a,b)] from BINOP_1:sch_3(A1);
take  o ; ::_thesis: for x, y being Element of OSSub U0
for U1, U2 being strict OSSubAlgebra of U0 st x = U1 & y = U2 holds
o . (x,y) = U1 /\ U2
thus  for x, y being Element of OSSub U0
for U1, U2 being strict OSSubAlgebra of U0 st x = U1 & y = U2 holds
o . (x,y) = U1 /\ U2 by A2; ::_thesis: verum
end;
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 & y = U2 holds
b1 . (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
b2 . (x,y) = U1 /\ U2 ) holds
b1 = b2
proof
let o1, o2 be BinOp of (OSSub U0); ::_thesis: ( ( for x, y being Element of OSSub U0
for U1, U2 being strict OSSubAlgebra of U0 st x = U1 & y = U2 holds
o1 . (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
o2 . (x,y) = U1 /\ U2 ) implies o1 = o2 )
assume that
A3: for x, y being Element of OSSub U0
for U1, U2 being strict OSSubAlgebra of U0 st x = U1 & y = U2 holds
o1 . (x,y) = U1 /\ U2 and
A4: for x, y being Element of OSSub U0
for U1, U2 being strict OSSubAlgebra of U0 st x = U1 & y = U2 holds
o2 . (x,y) = U1 /\ U2 ; ::_thesis: o1 = o2
 for x, y being Element of OSSub U0 holds o1 . (x,y) = o2 . (x,y)
proof
let x, y be Element of OSSub U0; ::_thesis: o1 . (x,y) = o2 . (x,y)
reconsider U1 = x, U2 = y as strict OSSubAlgebra of U0 by Def14;
 o1 . (x,y) = U1 /\ U2 by A3;
hence  o1 . (x,y) = o2 . (x,y) by A4; ::_thesis: verum
end;
hence  o1 = o2 by BINOP_1:2; ::_thesis: verum
end;
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 & 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)
proof
let S1 be OrderSortedSign; ::_thesis: 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)
let U0 be non-empty OSAlgebra of S1; ::_thesis: for x, y being Element of OSSub U0 holds (OSAlg_meet U0) . (x,y) = (MSAlg_meet U0) . (x,y)
let x, y be Element of OSSub U0; ::_thesis: (OSAlg_meet U0) . (x,y) = (MSAlg_meet U0) . (x,y)
 ( x is strict OSSubAlgebra of U0 & y is strict OSSubAlgebra of U0 ) by Def14;
then consider U1, U2 being strict OSSubAlgebra of U0 such that
A1: ( x = U1 & y = U2 ) ;
(OSAlg_meet U0) . (x,y) = U1 /\ U2 by A1, Def16
.= (MSAlg_meet U0) . (x,y) by A1, MSUALG_2:def_21 ;
hence  (OSAlg_meet U0) . (x,y) = (MSAlg_meet U0) . (x,y) ; ::_thesis: verum
end;

theorem Th44: :: OSALG_2:44
for S1 being OrderSortedSign
for U0 being non-empty OSAlgebra of S1 holds OSAlg_join U0 is commutative
proof
let S1 be OrderSortedSign; ::_thesis: for U0 being non-empty OSAlgebra of S1 holds OSAlg_join U0 is commutative
let U0 be non-empty OSAlgebra of S1; ::_thesis: OSAlg_join U0 is commutative
set o = OSAlg_join U0;
 for x, y being Element of OSSub U0 holds (OSAlg_join U0) . (x,y) = (OSAlg_join U0) . (y,x)
proof
let x, y be Element of OSSub U0; ::_thesis: (OSAlg_join U0) . (x,y) = (OSAlg_join U0) . (y,x)
reconsider U1 = x, U2 = y as strict OSSubAlgebra of U0 by Def14;
set B = the Sorts of U1 \/ the Sorts of U2;
 the Sorts of U2 is MSSubset of U0 by MSUALG_2:def_9;
then A1: the Sorts of U2 c= the Sorts of U0 by PBOOLE:def_18;
 the Sorts of U1 is MSSubset of U0 by MSUALG_2:def_9;
then  the Sorts of U1 c= the Sorts of U0 by PBOOLE:def_18;
then  the Sorts of U1 \/ the Sorts of U2 c= the Sorts of U0 by A1, PBOOLE:16;
then A2: the Sorts of U1 \/ the Sorts of U2 is MSSubset of U0 by PBOOLE:def_18;
 ( the Sorts of U1 is OrderSortedSet of S1 & the Sorts of U2 is OrderSortedSet of S1 ) by OSALG_1:17;
then  the Sorts of U1 \/ the Sorts of U2 is OrderSortedSet of S1 by Th2;
then reconsider B = the Sorts of U1 \/ the Sorts of U2 as OSSubset of U0 by A2, Def2;
A3: U1 "\/"_os U2 = GenOSAlg B by Def13;
 ( (OSAlg_join U0) . (x,y) = U1 "\/"_os U2 & (OSAlg_join U0) . (y,x) = U2 "\/"_os U1 ) by Def15;
hence  (OSAlg_join U0) . (x,y) = (OSAlg_join U0) . (y,x) by A3, Def13; ::_thesis: verum
end;
hence  OSAlg_join U0 is commutative by BINOP_1:def_2; ::_thesis: verum
end;

theorem Th45: :: OSALG_2:45
for S1 being OrderSortedSign
for U0 being non-empty OSAlgebra of S1 holds OSAlg_join U0 is associative
proof
let S1 be OrderSortedSign; ::_thesis: for U0 being non-empty OSAlgebra of S1 holds OSAlg_join U0 is associative
let U0 be non-empty OSAlgebra of S1; ::_thesis: OSAlg_join U0 is associative
set o = OSAlg_join U0;
 for x, y, z being Element of OSSub U0 holds (OSAlg_join U0) . (x,((OSAlg_join U0) . (y,z))) = (OSAlg_join U0) . (((OSAlg_join U0) . (x,y)),z)
proof
let x, y, z be Element of OSSub U0; ::_thesis: (OSAlg_join U0) . (x,((OSAlg_join U0) . (y,z))) = (OSAlg_join U0) . (((OSAlg_join U0) . (x,y)),z)
reconsider U1 = x, U2 = y, U3 = z as strict OSSubAlgebra of U0 by Def14;
set B = the Sorts of U1 \/ ( the Sorts of U2 \/ the Sorts of U3);
A1: the Sorts of U2 is OrderSortedSet of S1 by OSALG_1:17;
 the Sorts of U2 is MSSubset of U0 by MSUALG_2:def_9;
then A2: the Sorts of U2 c= the Sorts of U0 by PBOOLE:def_18;
 the Sorts of U3 is MSSubset of U0 by MSUALG_2:def_9;
then  the Sorts of U3 c= the Sorts of U0 by PBOOLE:def_18;
then A3: the Sorts of U2 \/ the Sorts of U3 c= the Sorts of U0 by A2, PBOOLE:16;
then reconsider C1 = the Sorts of U2 \/ the Sorts of U3 as MSSubset of U0 by PBOOLE:def_18;
 the Sorts of U3 is OrderSortedSet of S1 by OSALG_1:17;
then A4: the Sorts of U2 \/ the Sorts of U3 is OrderSortedSet of S1 by A1, Th2;
then reconsider C = C1 as OSSubset of U0 by Def2;
A5: the Sorts of U1 is OrderSortedSet of S1 by OSALG_1:17;
then A6: the Sorts of U1 \/ ( the Sorts of U2 \/ the Sorts of U3) is OrderSortedSet of S1 by A4, Th2;
 the Sorts of U1 is MSSubset of U0 by MSUALG_2:def_9;
then A7: the Sorts of U1 c= the Sorts of U0 by PBOOLE:def_18;
then  the Sorts of U1 \/ the Sorts of U2 c= the Sorts of U0 by A2, PBOOLE:16;
then reconsider D1 = the Sorts of U1 \/ the Sorts of U2 as MSSubset of U0 by PBOOLE:def_18;
 (OSAlg_join U0) . (y,z) = U2 "\/"_os U3 by Def15;
then A8: (OSAlg_join U0) . (x,((OSAlg_join U0) . (y,z))) = U1 "\/"_os (U2 "\/"_os U3) by Def15;
 the Sorts of U1 \/ the Sorts of U2 is OrderSortedSet of S1 by A5, A1, Th2;
then reconsider D = D1 as OSSubset of U0 by Def2;
A9: (OSAlg_join U0) . (x,y) = U1 "\/"_os U2 by Def15;
 the Sorts of U1 \/ ( the Sorts of U2 \/ the Sorts of U3) c= the Sorts of U0 by A7, A3, PBOOLE:16;
then  the Sorts of U1 \/ ( the Sorts of U2 \/ the Sorts of U3) is MSSubset of U0 by PBOOLE:def_18;
then reconsider B = the Sorts of U1 \/ ( the Sorts of U2 \/ the Sorts of U3) as OSSubset of U0 by A6, Def2;
A10: B = D \/ the Sorts of U3 by PBOOLE:28;
A11: (U1 "\/"_os U2) "\/"_os U3 = (GenOSAlg D) "\/"_os U3 by Def13
.= GenOSAlg B by A10, Th37 ;
U1 "\/"_os (U2 "\/"_os U3) = U1 "\/"_os (GenOSAlg C) by Def13
.= (GenOSAlg C) "\/"_os U1 by Th39
.= GenOSAlg B by Th37 ;
hence  (OSAlg_join U0) . (x,((OSAlg_join U0) . (y,z))) = (OSAlg_join U0) . (((OSAlg_join U0) . (x,y)),z) by A9, A8, A11, Def15; ::_thesis: verum
end;
hence  OSAlg_join U0 is associative by BINOP_1:def_3; ::_thesis: verum
end;

theorem Th46: :: OSALG_2:46
for S1 being OrderSortedSign
for U0 being non-empty OSAlgebra of S1 holds OSAlg_meet U0 is commutative
proof
let S1 be OrderSortedSign; ::_thesis: for U0 being non-empty OSAlgebra of S1 holds OSAlg_meet U0 is commutative
let U0 be non-empty OSAlgebra of S1; ::_thesis: OSAlg_meet U0 is commutative
set o = OSAlg_meet U0;
set m = MSAlg_meet U0;
A1: MSAlg_meet U0 is commutative by MSUALG_2:31;
 for x, y being Element of OSSub U0 holds (OSAlg_meet U0) . (x,y) = (OSAlg_meet U0) . (y,x)
proof
let x, y be Element of OSSub U0; ::_thesis: (OSAlg_meet U0) . (x,y) = (OSAlg_meet U0) . (y,x)
(OSAlg_meet U0) . (x,y) = (MSAlg_meet U0) . (x,y) by Th43
.= (MSAlg_meet U0) . (y,x) by A1, BINOP_1:def_2
.= (OSAlg_meet U0) . (y,x) by Th43 ;
hence  (OSAlg_meet U0) . (x,y) = (OSAlg_meet U0) . (y,x) ; ::_thesis: verum
end;
hence  OSAlg_meet U0 is commutative by BINOP_1:def_2; ::_thesis: verum
end;

theorem Th47: :: OSALG_2:47
for S1 being OrderSortedSign
for U0 being non-empty OSAlgebra of S1 holds OSAlg_meet U0 is associative
proof
let S1 be OrderSortedSign; ::_thesis: for U0 being non-empty OSAlgebra of S1 holds OSAlg_meet U0 is associative
let U0 be non-empty OSAlgebra of S1; ::_thesis: OSAlg_meet U0 is associative
set o = OSAlg_meet U0;
set m = MSAlg_meet U0;
A1: MSAlg_meet U0 is associative by MSUALG_2:32;
 for x, y, z being Element of OSSub U0 holds (OSAlg_meet U0) . (x,((OSAlg_meet U0) . (y,z))) = (OSAlg_meet U0) . (((OSAlg_meet U0) . (x,y)),z)
proof
let x, y, z be Element of OSSub U0; ::_thesis: (OSAlg_meet U0) . (x,((OSAlg_meet U0) . (y,z))) = (OSAlg_meet U0) . (((OSAlg_meet U0) . (x,y)),z)
A2: (OSAlg_meet U0) . (x,y) = (MSAlg_meet U0) . (x,y) by Th43;
 (OSAlg_meet U0) . (y,z) = (MSAlg_meet U0) . (y,z) by Th43;
then (OSAlg_meet U0) . (x,((OSAlg_meet U0) . (y,z))) = (MSAlg_meet U0) . (x,((MSAlg_meet U0) . (y,z))) by Th43
.= (MSAlg_meet U0) . (((MSAlg_meet U0) . (x,y)),z) by A1, BINOP_1:def_3
.= (OSAlg_meet U0) . (((OSAlg_meet U0) . (x,y)),z) by A2, Th43 ;
hence  (OSAlg_meet U0) . (x,((OSAlg_meet U0) . (y,z))) = (OSAlg_meet U0) . (((OSAlg_meet U0) . (x,y)),z) ; ::_thesis: verum
end;
hence  OSAlg_meet U0 is associative by BINOP_1:def_3; ::_thesis: verum
end;

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
proof
set L = LattStr(# (OSSub U0),(OSAlg_join U0),(OSAlg_meet U0) #);
A1: for a, b, c being Element of LattStr(# (OSSub U0),(OSAlg_join U0),(OSAlg_meet U0) #) holds a "\/" (b "\/" c) = (a "\/" b) "\/" c
proof
let a, b, c be Element of LattStr(# (OSSub U0),(OSAlg_join U0),(OSAlg_meet U0) #); ::_thesis: a "\/" (b "\/" c) = (a "\/" b) "\/" c
 OSAlg_join U0 is associative by Th45;
hence  a "\/" (b "\/" c) = (a "\/" b) "\/" c by BINOP_1:def_3; ::_thesis: verum
end;
A2: for a, b being Element of LattStr(# (OSSub U0),(OSAlg_join U0),(OSAlg_meet U0) #) holds a "/\" b = b "/\" a
proof
let a, b be Element of LattStr(# (OSSub U0),(OSAlg_join U0),(OSAlg_meet U0) #); ::_thesis: a "/\" b = b "/\" a
 OSAlg_meet U0 is commutative by Th46;
hence  a "/\" b = b "/\" a by BINOP_1:def_2; ::_thesis: verum
end;
A3: for a, b being Element of LattStr(# (OSSub U0),(OSAlg_join U0),(OSAlg_meet U0) #) holds a "/\" (a "\/" b) = a
proof
let a, b be Element of LattStr(# (OSSub U0),(OSAlg_join U0),(OSAlg_meet U0) #); ::_thesis: a "/\" (a "\/" b) = a
reconsider x = a, y = b as Element of OSSub U0 ;
 (OSAlg_meet U0) . (x,((OSAlg_join U0) . (x,y))) = x
proof
reconsider U1 = x, U2 = y as strict OSSubAlgebra of U0 by Def14;
 (OSAlg_join U0) . (x,y) = U1 "\/"_os U2 by Def15;
hence (OSAlg_meet U0) . (x,((OSAlg_join U0) . (x,y))) = U1 /\ (U1 "\/"_os U2) by Def16
.= x by Th40 ;
::_thesis: verum
end;
hence  a "/\" (a "\/" b) = a ; ::_thesis: verum
end;
A4: for a, b being Element of LattStr(# (OSSub U0),(OSAlg_join U0),(OSAlg_meet U0) #) holds (a "/\" b) "\/" b = b
proof
let a, b be Element of LattStr(# (OSSub U0),(OSAlg_join U0),(OSAlg_meet U0) #); ::_thesis: (a "/\" b) "\/" b = b
reconsider x = a, y = b as Element of OSSub U0 ;
 (OSAlg_join U0) . (((OSAlg_meet U0) . (x,y)),y) = y
proof
reconsider U1 = x, U2 = y as strict OSSubAlgebra of U0 by Def14;
 (OSAlg_meet U0) . (x,y) = U1 /\ U2 by Def16;
hence (OSAlg_join U0) . (((OSAlg_meet U0) . (x,y)),y) = (U1 /\ U2) "\/"_os U2 by Def15
.= y by Th41 ;
::_thesis: verum
end;
hence  (a "/\" b) "\/" b = b ; ::_thesis: verum
end;
A5: for a, b, c being Element of LattStr(# (OSSub U0),(OSAlg_join U0),(OSAlg_meet U0) #) holds a "/\" (b "/\" c) = (a "/\" b) "/\" c
proof
let a, b, c be Element of LattStr(# (OSSub U0),(OSAlg_join U0),(OSAlg_meet U0) #); ::_thesis: a "/\" (b "/\" c) = (a "/\" b) "/\" c
 OSAlg_meet U0 is associative by Th47;
hence  a "/\" (b "/\" c) = (a "/\" b) "/\" c by BINOP_1:def_3; ::_thesis: verum
end;
 for a, b being Element of LattStr(# (OSSub U0),(OSAlg_join U0),(OSAlg_meet U0) #) holds a "\/" b = b "\/" a
proof
let a, b be Element of LattStr(# (OSSub U0),(OSAlg_join U0),(OSAlg_meet U0) #); ::_thesis: a "\/" b = b "\/" a
 OSAlg_join U0 is commutative by Th44;
hence  a "\/" b = b "\/" a by BINOP_1:def_2; ::_thesis: verum
end;
then  ( LattStr(# (OSSub U0),(OSAlg_join U0),(OSAlg_meet U0) #) is strict & LattStr(# (OSSub U0),(OSAlg_join U0),(OSAlg_meet U0) #) is join-commutative & LattStr(# (OSSub U0),(OSAlg_join U0),(OSAlg_meet U0) #) is join-associative & LattStr(# (OSSub U0),(OSAlg_join U0),(OSAlg_meet U0) #) is meet-absorbing & LattStr(# (OSSub U0),(OSAlg_join U0),(OSAlg_meet U0) #) is meet-commutative & LattStr(# (OSSub U0),(OSAlg_join U0),(OSAlg_meet U0) #) is meet-associative & LattStr(# (OSSub U0),(OSAlg_join U0),(OSAlg_meet U0) #) is join-absorbing ) by A1, A4, A2, A5, A3, LATTICES:def_4, LATTICES:def_5, LATTICES:def_6, LATTICES:def_7, LATTICES:def_8, LATTICES:def_9;
hence  LattStr(# (OSSub U0),(OSAlg_join U0),(OSAlg_meet U0) #) is strict Lattice ; ::_thesis: verum
end;
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
proof
let S1 be OrderSortedSign; ::_thesis: for U0 being non-empty OSAlgebra of S1 holds OSSubAlLattice U0 is bounded
let U0 be non-empty OSAlgebra of S1; ::_thesis: OSSubAlLattice U0 is bounded
set L = OSSubAlLattice U0;
thus  OSSubAlLattice U0 is lower-bounded :: according to LATTICES:def_15 ::_thesis: OSSubAlLattice U0 is upper-bounded
proof
set C = OSConstants U0;
reconsider G = GenOSAlg (OSConstants U0) as Element of OSSub U0 by Def14;
reconsider G1 = G as Element of (OSSubAlLattice U0) ;
take  G1 ; :: according to LATTICES:def_13 ::_thesis: for b1 being Element of the carrier of (OSSubAlLattice U0) holds
( G1 "/\" b1 = G1 & b1 "/\" G1 = G1 )
let a be Element of (OSSubAlLattice U0); ::_thesis: ( G1 "/\" a = G1 & a "/\" G1 = G1 )
reconsider a1 = a as Element of OSSub U0 ;
reconsider a2 = a1 as strict OSSubAlgebra of U0 by Def14;
thus G1 "/\" a = (GenOSAlg (OSConstants U0)) /\ a2 by Def16
.= G1 by Th36 ; ::_thesis: a "/\" G1 = G1
hence  a "/\" G1 = G1 ; ::_thesis: verum
end;
thus  OSSubAlLattice U0 is upper-bounded ::_thesis: verum
proof
reconsider B = the Sorts of U0 as MSSubset of U0 by PBOOLE:def_18;
 the Sorts of U0 is OrderSortedSet of S1 by OSALG_1:17;
then reconsider B = B as OSSubset of U0 by Def2;
reconsider G = GenOSAlg B as Element of OSSub U0 by Def14;
reconsider G1 = G as Element of (OSSubAlLattice U0) ;
take  G1 ; :: according to LATTICES:def_14 ::_thesis: for b1 being Element of the carrier of (OSSubAlLattice U0) holds
( G1 "\/" b1 = G1 & b1 "\/" G1 = G1 )
let a be Element of (OSSubAlLattice U0); ::_thesis: ( G1 "\/" a = G1 & a "\/" G1 = G1 )
reconsider a1 = a as Element of OSSub U0 ;
reconsider a2 = a1 as strict OSSubAlgebra of U0 by Def14;
thus G1 "\/" a = (GenOSAlg B) "\/"_os a2 by Def15
.= G1 by Th38 ; ::_thesis: a "\/" G1 = G1
hence  a "\/" G1 = G1 ; ::_thesis: verum
end;
end;

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)
proof
let S1 be OrderSortedSign; ::_thesis: for U0 being non-empty OSAlgebra of S1 holds Bottom (OSSubAlLattice U0) = GenOSAlg (OSConstants U0)
let U0 be non-empty OSAlgebra of S1; ::_thesis: Bottom (OSSubAlLattice U0) = GenOSAlg (OSConstants U0)
set C = OSConstants U0;
reconsider G = GenOSAlg (OSConstants U0) as Element of OSSub U0 by Def14;
set L = OSSubAlLattice U0;
reconsider G1 = G as Element of (OSSubAlLattice U0) ;
now__::_thesis:_for_a_being_Element_of_(OSSubAlLattice_U0)_holds_
(_G1_"/\"_a_=_G1_&_a_"/\"_G1_=_G1_)
let a be Element of (OSSubAlLattice U0); ::_thesis: ( G1 "/\" a = G1 & a "/\" G1 = G1 )
reconsider a1 = a as Element of OSSub U0 ;
reconsider a2 = a1 as strict OSSubAlgebra of U0 by Def14;
thus G1 "/\" a = (GenOSAlg (OSConstants U0)) /\ a2 by Def16
.= G1 by Th36 ; ::_thesis: a "/\" G1 = G1
hence  a "/\" G1 = G1 ; ::_thesis: verum
end;
hence  Bottom (OSSubAlLattice U0) = GenOSAlg (OSConstants U0) by LATTICES:def_16; ::_thesis: verum
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
proof
let S1 be OrderSortedSign; ::_thesis: 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
let U0 be non-empty OSAlgebra of S1; ::_thesis: for B being OSSubset of U0 st B = the Sorts of U0 holds
Top (OSSubAlLattice U0) = GenOSAlg B
let B be OSSubset of U0; ::_thesis: ( B = the Sorts of U0 implies Top (OSSubAlLattice U0) = GenOSAlg B )
reconsider G = GenOSAlg B as Element of OSSub U0 by Def14;
set L = OSSubAlLattice U0;
reconsider G1 = G as Element of (OSSubAlLattice U0) ;
assume A1: B = the Sorts of U0 ; ::_thesis: Top (OSSubAlLattice U0) = GenOSAlg B
now__::_thesis:_for_a_being_Element_of_(OSSubAlLattice_U0)_holds_
(_G1_"\/"_a_=_G1_&_a_"\/"_G1_=_G1_)
let a be Element of (OSSubAlLattice U0); ::_thesis: ( G1 "\/" a = G1 & a "\/" G1 = G1 )
reconsider a1 = a as Element of OSSub U0 ;
reconsider a2 = a1 as strict OSSubAlgebra of U0 by Def14;
thus G1 "\/" a = (GenOSAlg B) "\/"_os a2 by Def15
.= G1 by A1, Th38 ; ::_thesis: a "\/" G1 = G1
hence  a "\/" G1 = G1 ; ::_thesis: verum
end;
hence  Top (OSSubAlLattice U0) = GenOSAlg B by LATTICES:def_17; ::_thesis: verum
end;

theorem :: OSALG_2:51
for S1 being OrderSortedSign
for U0 being strict non-empty OSAlgebra of S1 holds Top (OSSubAlLattice U0) = U0
proof
let S1 be OrderSortedSign; ::_thesis: for U0 being strict non-empty OSAlgebra of S1 holds Top (OSSubAlLattice U0) = U0
let U0 be strict non-empty OSAlgebra of S1; ::_thesis: Top (OSSubAlLattice U0) = U0
reconsider B = the Sorts of U0 as MSSubset of U0 by PBOOLE:def_18;
 B is OrderSortedSet of S1 by OSALG_1:17;
then reconsider B = the Sorts of U0 as OSSubset of U0 by Def2;
thus  Top (OSSubAlLattice U0) = GenOSAlg B by Th50
.= U0 by Th34 ; ::_thesis: verum
end;