The Mizar article:

Subalgebras of an Order Sorted Algebra. Lattice of Subalgebras

by
Josef Urban

Received September 19, 2002

Copyright (c) 2002 Association of Mizar Users

MML identifier: OSALG_2
[ MML identifier index ]


environ

 vocabulary FUNCT_1, RELAT_1, PBOOLE, ZF_REFLE, BOOLE, CARD_3, AMI_1, MSUALG_1,
      UNIALG_2, TDGROUP, QC_LANG1, PRALG_1, PROB_1, TARSKI, SETFAM_1, LATTICES,
      BINOP_1, MSUALG_2, OSALG_1, ORDERS_1, SEQM_3, OSALG_2;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, STRUCT_0, RELAT_1, FUNCT_1,
      SETFAM_1, LATTICES, BINOP_1, PROB_1, CARD_3, MBOOLEAN, PBOOLE, MSUALG_1,
      ORDERS_1, MSUALG_2, YELLOW18, OSALG_1;
 constructors MBOOLEAN, PROB_1, ORDERS_3, OSALG_1, YELLOW18, MSUALG_2;
 clusters FUNCT_1, LATTICES, MSUALG_1, RELSET_1, STRUCT_0, RLSUB_2, SUBSET_1,
      ORDERS_3, OSALG_1, MSUALG_2, MSAFREE, XBOOLE_0;
 requirements BOOLE, SUBSET;
 definitions TARSKI, PBOOLE, LATTICES, OSALG_1, MSUALG_2;
 theorems TARSKI, XBOOLE_0, XBOOLE_1, FUNCT_1, RELSET_1, PBOOLE, CARD_3,
      MSUALG_1, FUNCT_2, ZFMISC_1, SETFAM_1, BINOP_1, LATTICES, RELAT_1,
      PROB_1, OSALG_1, ORDERS_1, MSUALG_2, MBOOLEAN;
 schemes XBOOLE_0, BINOP_1, MSUALG_2;

begin :: Auxiliary facts about Order Sorted Sets.

reserve x for set,
        R for non empty Poset;

:: should be clusters, but that requires redef of the operation
theorem Th1:
  for X,Y being OrderSortedSet of R holds X /\ Y is OrderSortedSet of R
proof
  let X,Y be OrderSortedSet of R;
  reconsider M = X /\ Y as ManySortedSet of R;
    M is order-sorted
  proof
    let s1,s2 be Element of R;
    assume A1: s1 <= s2;
    A2: (X /\ Y).s1 = X.s1 /\ Y.s1 &
    (X /\ Y).s2 = X.s2 /\ Y.s2 by PBOOLE:def 8;
      X.s1 c= X.s2 & Y.s1 c= Y.s2 by A1,OSALG_1:def 18;
    hence thesis by A2,XBOOLE_1:27;
  end;
  hence thesis;
end;

theorem Th2:
  for X,Y being OrderSortedSet of R holds X \/ Y is OrderSortedSet of R
proof
  let X,Y be OrderSortedSet of R;
  reconsider M = X \/ Y as ManySortedSet of R;
    M is order-sorted
  proof
    let s1,s2 be Element of R;
    assume A1: s1 <= s2;
    A2: (X \/ Y).s1 = X.s1 \/ Y.s1 &
    (X \/ Y).s2 = X.s2 \/ Y.s2 by PBOOLE:def 7;
      X.s1 c= X.s2 & Y.s1 c= Y.s2 by A1,OSALG_1:def 18;
    hence thesis by A2,XBOOLE_1:13;
  end;
  hence thesis;
end;

:: new and bad
definition let R be non empty Poset,
               M be OrderSortedSet of R; :: can be for ManySortedSet
  mode OrderSortedSubset of M -> ManySortedSubset of M means :Def1:
  it is OrderSortedSet of R;
  existence
  proof
    reconsider X=M as ManySortedSubset of M by MSUALG_2:def 1;
    take X;
    thus thesis;
  end;
end;

definition let R be non empty Poset,
               M be non-empty OrderSortedSet of R;
cluster non-empty OrderSortedSubset of M;
 existence
  proof
   reconsider N= M as ManySortedSubset of M by MSUALG_2:def 1;
   reconsider N1 = N as OrderSortedSubset of M by Def1;
   take N1;
   thus thesis;
  end;
end;

begin
::
::  Constants of an Order Sorted Algebra.
::

definition let S be OrderSortedSign,
              U0 be OSAlgebra of S;
 mode OSSubset of U0 -> ManySortedSubset of the Sorts of U0 means :Def2:
  it is OrderSortedSet of S;
existence
proof
  reconsider B = the Sorts of U0 as MSSubset of U0 by MSUALG_2:def 1;
  take B;
  thus B is OrderSortedSet of S by OSALG_1:17;
end;
end;

:: very strange, the cluster in OSALG_1 should take care of this one
definition let S be OrderSortedSign;
  cluster monotone strict non-empty OSAlgebra of S;
  existence
   proof
    consider z being non empty set;
    consider z1 being Element of z;
    take TrivialOSA(S,z,z1);
    thus thesis;
  end;
end;

definition
  let S be OrderSortedSign,
      U0 be non-empty OSAlgebra of S;
cluster non-empty OSSubset of U0;
 existence
  proof
    A1: the Sorts of U0 is OrderSortedSet of S by OSALG_1:17;
    reconsider N= the Sorts of U0 as MSSubset of U0 by MSUALG_2:def 1;
    reconsider M = N as OSSubset of U0 by A1,Def2;
    take M;
    thus thesis;
  end;
end;

theorem Th3:
  for S0 being non void all-with_const_op strict (non empty ManySortedSign)
  holds OSSign S0 is all-with_const_op
proof
  let S0 be non void all-with_const_op strict (non empty ManySortedSign);
  let s be Element of OSSign S0;
  reconsider s1 =s as Element of S0 by OSALG_1:def 6;
    s1 is with_const_op by MSUALG_2:def 3;
  then consider o being Element of the OperSymbols of S0 such that
  A1: (the Arity of S0).o = {} & (the ResultSort of S0).o = s1
  by MSUALG_2:def 2;
    o is Element of the OperSymbols of OSSign S0 &
  (the Arity of OSSign S0).o = {} &
  (the ResultSort of OSSign S0).o = s1 by A1,OSALG_1:def 6;
  hence s is with_const_op by MSUALG_2:def 2;
end;

definition
  cluster all-with_const_op strict OrderSortedSign;
  existence
  proof consider S0 being
    non void all-with_const_op strict (non empty ManySortedSign);
    take OSSign S0;
    thus thesis by Th3;
  end;
end;

begin
::
::   Subalgebras of a Order Sorted Algebra.
::

theorem Th4:
 for S being OrderSortedSign,
     U0 being OSAlgebra of S holds
 MSAlgebra (#the Sorts of U0,the Charact of U0#) is order-sorted
proof
  let S be OrderSortedSign,
  U0 be OSAlgebra of S;
  set U1 = MSAlgebra (#the Sorts of U0,the Charact of U0#);
    the Sorts of U0 is OrderSortedSet of S by OSALG_1:17;
  hence U1 is order-sorted by OSALG_1:17;
end;

definition let S be OrderSortedSign,
               U0 be OSAlgebra of S; :: can't for ms!
  cluster order-sorted MSSubAlgebra of U0;
  existence
  proof
    reconsider U1 = MSAlgebra (#the Sorts of U0,the Charact of U0#)
    as strict MSSubAlgebra of U0 by MSUALG_2:38;
    take U1;
    thus thesis by Th4;
  end;
end;

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

definition let S be OrderSortedSign,
               U0 be OSAlgebra of S;
cluster strict OSSubAlgebra of U0;
 existence
 proof
   reconsider U1 = MSAlgebra (#the Sorts of U0,the Charact of U0#)
    as order-sorted MSSubAlgebra of U0 by Th4,MSUALG_2:38;
    take U1;
    thus thesis;
  end;
end;

definition let S be OrderSortedSign,
               U0 be non-empty OSAlgebra of S;
cluster non-empty strict OSSubAlgebra of U0;
 existence
 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 as strict OSSubAlgebra of U0 by MSUALG_2:38,OSALG_1:17;
   take U1;
   thus thesis;
 end;
end;

:: the equivalent def, maybe not needed
theorem Th5:
  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 be 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;
  let U0 be OSAlgebra of S;
  let U1 be MSAlgebra over S;
  hereby
    assume A1: U1 is OSSubAlgebra of U0;
    then A2: the Sorts of U1 is OrderSortedSet of S by OSALG_1:17;
      the Sorts of U1 is MSSubset of U0 by A1,MSUALG_2:def 10;
    hence the Sorts of U1 is OSSubset of U0
    by A2,Def2;
    let B be OSSubset of U0 such that A3: B = the Sorts of U1;
    thus B is opers_closed & the Charact of U1 = Opers(U0,B)
    by A1,A3,MSUALG_2:def 10;
  end;
  assume A4: the Sorts of U1 is OSSubset of U0;
  then A5: the Sorts of U1 is OrderSortedSet of S by Def2;
  assume A6:
    for B be OSSubset of U0 st B = the Sorts of U1 holds
    B is opers_closed & the Charact of U1 = Opers(U0,B);
    U1 is MSSubAlgebra of U0
  proof
    thus the Sorts of U1 is MSSubset of U0 by A4;
    let B be MSSubset of U0 such that A7: B = the Sorts of U1;
    reconsider B1=B as OSSubset of U0 by A4,A7;
      B1 is opers_closed & the Charact of U1 = Opers(U0,B1) by A6,A7;
    hence thesis;
  end;
  hence thesis by A5,OSALG_1:17;
end;

reserve S1 for OrderSortedSign,
        OU0 for OSAlgebra of S1;
reserve s,s1,s2,s3,s4 for SortSymbol of S1;

definition let S1,OU0,s;
  func OSConstants(OU0,s) -> Subset of (the Sorts of OU0).s equals
  :Def3: union {Constants(OU0,s2) : s2 <= s};
  coherence
  proof
    set Cs = {Constants(OU0,s2) : s2 <= s};
      for X being set st X in Cs holds X c= (the Sorts of OU0).s
    proof let X be set such that A1: X in Cs;
      consider s2 such that A2: X = Constants(OU0,s2) & s2 <= s by A1;
        (the Sorts of OU0).s2 c= (the Sorts of OU0).s
      by A2,OSALG_1:def 19;
      hence thesis by A2,XBOOLE_1:1;
    end;
    hence thesis by ZFMISC_1:94;
  end;
end;

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

canceled 5;

theorem Th11:
  Constants(OU0,s) c= OSConstants(OU0,s)
proof
    Constants(OU0,s) in {Constants(OU0,s2) : s2 <= s};
  then Constants(OU0,s) c= union {Constants(OU0,s2) : s2 <= s} by ZFMISC_1:92;
  hence thesis by Def3;
end;

definition let S1;
  let M be ManySortedSet of the carrier of S1;
  func OSCl M -> OrderSortedSet of S1 means :Def4:
  for s be SortSymbol of S1 holds it.s = union { M.s1: s1 <= s};
  existence
  proof
    deffunc F(Element of S1) = union {M.s1: s1 <= $1};
    consider f be Function such that A1:dom f = the carrier of S1 &
    for d be Element of S1 holds f.d = F(d) from LambdaB;
    reconsider f as ManySortedSet of the carrier of S1 by A1,PBOOLE:def 3;
    reconsider f1=f as ManySortedSet of S1;
      f1 is order-sorted
    proof
      let r1,r2 be Element of S1;
      assume A2: r1 <= r2;
      let x be set such that A3: x in f1.r1;
        x in union {M.s2: s2 <= r1} by A1,A3;
      then consider y being set such that A4: x in y &
      y in {M.s2: s2 <= r1} by TARSKI:def 4;
      consider s3 such that A5: y = M.s3 &
      s3 <= r1 by A4;
        s3 <= r2 by A2,A5,ORDERS_1:26;
      then y in {M.s2: s2 <= r2} by A5;
      then x in union {M.s2: s2 <= r2} by A4,TARSKI:def 4;
      hence x in f1.r2 by A1;
    end;
    then reconsider f2 = f1 as OrderSortedSet of S1;
    take f2;
    thus thesis by A1;
  end;
  uniqueness
  proof
    let W1, W2 be OrderSortedSet of S1;
    assume A6: (for s being SortSymbol of S1 holds
    W1.s = union { M.s1: s1 <= s} );
    assume A7: (for s being SortSymbol of S1 holds
    W2.s = union { M.s1: s1 <= s} );
      for s be set st s in the carrier of S1 holds W1.s = W2.s
    proof let s be set;
      assume s in the carrier of S1;
      then reconsider t = s as SortSymbol of S1;
        W1.s = union { M.s1: s1 <= t} by A6 .= W2.s by A7;
      hence thesis;
    end;
   hence thesis by PBOOLE:3;
  end;
end;

theorem Th12:
  for M being ManySortedSet of the carrier of S1 holds
  M c= OSCl M
proof
  let M be ManySortedSet of the carrier of S1;
  let i be set;
  assume i in the carrier of S1;
  then reconsider s = i as SortSymbol of S1;
    M.s in {M.s1: s1 <= s};
  then M.s c= union { M.s1: s1 <= s} by ZFMISC_1:92;
  hence thesis by Def4;
end;

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

theorem
    for S being OrderSortedSign,
      X being OrderSortedSet of S holds OSCl X = X
proof
  let S be OrderSortedSign,
      X be OrderSortedSet of S;
    X c= OSCl X & OSCl X c= X by Th12,Th13;
  hence thesis by PBOOLE:def 13;
end;

:: following should be rewritten to use OSCl Constants(OU0) instead;
:: maybe later
definition let S1,OU0;
func OSConstants (OU0) -> OSSubset of OU0 means :Def5:
 for s be SortSymbol of S1 holds it.s = OSConstants(OU0,s);
  existence
  proof
   deffunc F(Element of S1) =
     union {Constants(OU0,s1): s1 <= $1};
   consider f be Function such that A1:dom f = the carrier of S1 &
   for d be Element of S1 holds
   f.d = F(d) from LambdaB;
   reconsider f as ManySortedSet of the carrier of S1 by A1,PBOOLE:def 3;
     f c= the Sorts of OU0
    proof let s be set;
     assume s in the carrier of S1;
     then reconsider s1 = s as SortSymbol of S1;
       f.s1 = union {Constants(OU0,s2): s2 <= s1} by A1
     .= OSConstants(OU0,s1) by Def3;
     hence thesis;
    end;
    then reconsider f as MSSubset of OU0 by MSUALG_2:def 1;
   take f;
   reconsider f1=f as ManySortedSet of S1;
     f1 is order-sorted
   proof let r1,r2 be Element of S1;
     assume A2: r1 <= r2;
     let x be set such that A3: x in f1.r1;
       x in union {Constants(OU0,s2): s2 <= r1} by A1,A3;
     then consider y being set such that A4: x in y &
     y in {Constants(OU0,s2): s2 <= r1} by TARSKI:def 4;
     consider s3 such that A5: y = Constants(OU0,s3) &
     s3 <= r1 by A4;
       s3 <= r2 by A2,A5,ORDERS_1:26;
     then y in {Constants(OU0,s2): s2 <= r2} by A5;
     then x in union {Constants(OU0,s2): s2 <= r2} by A4,TARSKI:def 4;
     hence x in f1.r2 by A1;
   end;
   hence f is OSSubset of OU0 by Def2;
   thus for s being SortSymbol of S1 holds f.s = OSConstants(OU0,s)
   proof let s be SortSymbol of S1;
       f.s = union {Constants(OU0,s2): s2 <= s} by A1 .=
     OSConstants(OU0,s) by Def3;
     hence thesis;
   end;
 end;
 uniqueness
  proof let W1, W2 be OSSubset of OU0;
   assume A6: (for s be SortSymbol of S1 holds
   W1.s = OSConstants(OU0,s)) &
   for s be SortSymbol of S1 holds W2.s = OSConstants(OU0,s);
     for s be set st s in the carrier of S1 holds W1.s = W2.s
    proof let s be set;
     assume s in the carrier of S1;
     then reconsider t = s as SortSymbol of S1;
       W1.t = OSConstants(OU0,t) & W2.t = OSConstants(OU0,t) by A6;
     hence thesis;
    end;
   hence thesis by PBOOLE:3;
  end;
end;

theorem Th15:
  Constants(OU0) c= OSConstants(OU0)
proof
  let i be set;
  assume i in the carrier of S1;
  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 5;
  hence thesis by Th11;
end;

theorem Th16:
  for A being OSSubset of OU0 holds Constants(OU0) c= A implies
  OSConstants(OU0) c= A
proof
  let A be OSSubset of OU0;
  assume A1: Constants(OU0) c= A;
  A2: A is OrderSortedSet of S1 by Def2;
  assume not OSConstants(OU0) c= A;
  then consider i being set such that A3:
  i in the carrier of S1 and A4: not (OSConstants(OU0)).i c= A.i
  by PBOOLE:def 5;
  consider x being set such that A5: x in (OSConstants(OU0)).i
  and A6: not x in A.i by A4,TARSKI:def 3;
  reconsider s = i as SortSymbol of S1 by A3;
    (OSConstants(OU0)).s = OSConstants(OU0,s) by Def5 .=
  union {Constants(OU0,s2) : s2 <= s} by Def3;
  then consider X1 being set such that A7: x in X1 and
  A8: X1 in {Constants(OU0,s2) : s2 <= s} by A5,TARSKI:def 4;
  consider s1 being SortSymbol of S1 such that A9: X1 = Constants(OU0,s1)
  and A10: s1 <= s by A8;
  A11: (Constants(OU0)).s1 c= A.s1 by A1,PBOOLE:def 5;
  A12: A.s1 c= A.s by A2,A10,OSALG_1:def 18;
    x in (Constants(OU0)).s1 by A7,A9,MSUALG_2:def 5;
  then x in A.s1 by A11;
  hence contradiction by A6,A12;
end;

theorem
    for A being OSSubset of OU0 holds
  OSConstants(OU0) = OSCl Constants(OU0)
proof
  let A be OSSubset of OU0;
    now
    let i be set;
    assume i in the carrier of S1;
    then reconsider s = i as SortSymbol of S1;
    set c1 = { (Constants(OU0)).s1: s1 <= s},
        c2 = { Constants(OU0,s1): s1 <= s};
      for x being set holds (x in c1 iff x in c2)
    proof let x be set;
      hereby assume x in c1;
        then consider s1 such that A1: x = (Constants(OU0)).s1 & s1 <= s;
          x = Constants(OU0,s1) & s1 <= s by A1,MSUALG_2:def 5;
        hence x in c2;
      end;
      assume x in c2;
      then consider s1 such that A2: x = Constants(OU0,s1) & s1 <= s;
        x = (Constants(OU0)).s1 & s1 <= s by A2,MSUALG_2:def 5;
      hence x in c1;
    end;
    then A3: c1 = c2 by TARSKI:2;
      (OSConstants(OU0)).s = OSConstants(OU0,s) by Def5
    .= union { (Constants(OU0)).s1: s1 <= s} by A3,Def3 .=
    (OSCl Constants(OU0)).s by Def4;
    hence (OSConstants(OU0)).i = (OSCl Constants(OU0)).i;
  end;
  then ( for i being set st i in the carrier of S1 holds
    (OSConstants(OU0)).i c= (OSCl Constants(OU0)).i) &
    for i being set st i in the carrier of S1 holds
    (OSCl Constants(OU0)).i c= (OSConstants(OU0)).i;
  then OSConstants(OU0) c= OSCl Constants(OU0) &
  OSCl Constants(OU0) c= OSConstants(OU0) by PBOOLE:def 5;
  hence thesis by PBOOLE:def 13;
end;

theorem Th18:
  for OU1 being OSSubAlgebra of OU0 holds
  OSConstants(OU0) is OSSubset of OU1
proof
  let OU1 be OSSubAlgebra of OU0;
  A1: OSConstants(OU0) is ManySortedSubset of the Sorts of OU1
  proof
      OSConstants(OU0) c= the Sorts of OU1
    proof let i be set such that A2:
      i in the carrier of S1;
      reconsider s = i as SortSymbol of S1 by A2;
        Constants(OU0) is MSSubset of OU1 by MSUALG_2:11;
      then A3: Constants(OU0) c= (the Sorts of OU1) by MSUALG_2:def 1;
      A4: for s2,s3 st s2 <= s3 holds
      (Constants(OU0)).s2 c= (the Sorts of OU1).s3
      proof let s2,s3;
        assume s2 <= s3;
        then A5: (the Sorts of OU1).s2 c= (the Sorts of OU1).s3
        by OSALG_1:def 19;
          (Constants(OU0)).s2 c= (the Sorts of OU1).s2 by A3,PBOOLE:def 5;
        hence (Constants(OU0)).s2 c= (the Sorts of OU1).s3
        by A5,XBOOLE_1:1;
      end;
      A6: for X being set st X in {Constants(OU0,s1): s1 <= s} holds
      X c= (the Sorts of OU1).s
      proof let X be set;
        assume X in {Constants(OU0,s1): s1 <= s};
        then consider s4 such that A7: X = Constants(OU0,s4) &
        s4 <= s;
          Constants(OU0,s4) = (Constants(OU0)).s4 by MSUALG_2:def 5;
        hence thesis by A4,A7;
      end;
        (OSConstants(OU0)).i = OSConstants(OU0,s)
      by Def5 .= union {Constants(OU0,s1): s1 <= s} by Def3;
      hence (OSConstants(OU0)).i c= (the Sorts of OU1).i by A6,ZFMISC_1:94;
    end;
    hence thesis by MSUALG_2:def 1;
  end;
    OSConstants(OU0) is OrderSortedSet of S1 by Def2;
  hence thesis by A1,Def2;
end;

theorem
    for S being all-with_const_op OrderSortedSign,
  OU0 being non-empty OSAlgebra of S,
  OU1 being non-empty OSSubAlgebra of OU0 holds
  OSConstants(OU0) is non-empty OSSubset of OU1
proof
  let S be all-with_const_op OrderSortedSign,
      OU0 be non-empty OSAlgebra of S,
      OU1 be non-empty OSSubAlgebra of OU0;
    Constants(OU0) c= OSConstants(OU0) by Th15;
  hence thesis by Th18,PBOOLE:143;
end;

begin
::
::  Order Sorted Subsets of an Order Sorted Algebra.
::

:: this should be in MSUALG_2
theorem Th20:
  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;
  let M be ManySortedSet of I;
  let x be set;
  A1: I = dom bool M by PBOOLE:def 3;
  hereby
    assume x is ManySortedSubset of M;
    then reconsider x1 = x as ManySortedSubset of M;
    A2: dom x1 = I by PBOOLE:def 3 .= dom bool M by PBOOLE:def 3;
      for i being set st i in dom bool M holds x1.i in (bool M).i
    proof
      let i be set such that A3: i in dom bool M;
        x1 c= M by MSUALG_2:def 1;
      then x1.i c= M.i by A1,A3,PBOOLE:def 5;
      then x1.i in bool (M.i);
      hence x1.i in (bool M).i by A1,A3,MBOOLEAN:def 1;
    end;
    hence x in product bool M by A2,CARD_3:def 5;
  end;
  assume x in product bool M;
  then consider x1 being Function such that A4:
  x = x1 & dom x1 = dom bool M &
  for i being set st i in dom bool M holds x1.i in (bool M).i
  by CARD_3:def 5;
  reconsider x2 = x1 as ManySortedSet of I by A1,A4,PBOOLE:def 3;
    x2 c= M
  proof
    let i be set such that A5: i in I;
      x2.i in (bool M).i by A1,A4,A5;
    then x2.i in bool (M.i) by A5,MBOOLEAN:def 1;
    hence x2.i c= M.i;
  end;
  hence thesis by A4,MSUALG_2:def 1;
end;

:: Fraenkel should be improved, to allow more than just Element type
definition let R be non empty Poset,
  M be OrderSortedSet of R;
  func OSbool(M) -> set means
    for x being set holds x in it iff x is OrderSortedSubset of M;
  existence
  proof
    set f = product bool M;
    defpred P[set] means $1 is OrderSortedSubset of M;
    consider X being set such that
    A1: for y being set holds
    y in X iff y in f & P[y] from Separation;
    take X;
    let y be set;
    thus y in X implies y is OrderSortedSubset of M by A1;
    assume A2: y is OrderSortedSubset of M;
    then y in f by Th20;
    hence thesis by A1,A2;
  end;
  uniqueness
  proof
    defpred P[set] means $1 is OrderSortedSubset of M;
    thus for X1,X2 being set st
    (for x being set holds x in X1 iff P[x]) &
    (for x being set holds x in X2 iff P[x]) holds X1 = X2 from SetEq;
  end;
end;

definition let S be OrderSortedSign,
               U0 be OSAlgebra of S,
               A be OSSubset of U0;
func OSSubSort(A) -> set equals
:Def7: { x where x is Element of SubSort(A): x is OrderSortedSet of S};
correctness;
end;

theorem Th21:
  for A being OSSubset of OU0 holds OSSubSort(A) c= SubSort(A)
proof
  let A be OSSubset of OU0;
  let x be set such that A1: x in OSSubSort(A);
    x in { y where y is Element of SubSort(A): y is OrderSortedSet of S1}
  by A1,Def7;
  then consider y being Element of SubSort(A) such that A2: x = y &
  y is OrderSortedSet of S1;
  thus thesis by A2;
end;

theorem Th22:
  for A being OSSubset of OU0 holds the Sorts of OU0 in OSSubSort(A)
proof
  let A be OSSubset of OU0;
  reconsider X = the Sorts of OU0 as Element of SubSort(A) by MSUALG_2:40;
    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 thesis by Def7;
end;

definition let S1,OU0;
           let A be OSSubset of OU0;
  cluster OSSubSort(A) -> non empty;
  coherence by Th22;
end;

definition let S1,OU0;
  func OSSubSort(OU0) -> set equals :Def8:
{ x where x is Element of SubSort(OU0): x is OrderSortedSet of S1};
correctness;
end;

theorem Th23:
  for A being OSSubset of OU0 holds OSSubSort(A) c= OSSubSort(OU0)
proof
  let A be OSSubset of OU0;
  let x be set such that A1: x in OSSubSort(A);
    x in { y where y is Element of SubSort(A): y is OrderSortedSet of S1}
  by A1,Def7;
  then consider x1 being Element of SubSort(A) such that
  A2: x1 = x and A3: x1 is OrderSortedSet of S1;
    x1 in SubSort(A) & SubSort(A) c= SubSort(OU0) by MSUALG_2:41;
  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 A3;
  hence thesis by A2,Def8;
end;

definition let S1,OU0;
  cluster OSSubSort(OU0) -> non empty;
  coherence
  proof
    consider A being OSSubset of OU0;
      the Sorts of OU0 in OSSubSort(A) &
    OSSubSort(A) c= OSSubSort(OU0) by Th22,Th23;
    hence thesis;
  end;
end;

:: new-def for order-sorted
definition let S1,OU0;
           let e be Element of OSSubSort(OU0);
func @e -> OSSubset of OU0 equals :Def9:
 e;
 coherence
 proof
     e in OSSubSort(OU0);
   then e in
   { x where x is Element of SubSort(OU0): x is OrderSortedSet of S1}
   by Def8;
   then consider e1 being Element of SubSort(OU0) such that A1:
   e = e1 & e1 is OrderSortedSet of S1;
     e1 = @e1 by MSUALG_2:def 13;
   then reconsider e2 = @e1 as OSSubset of OU0 by A1,Def2;
     e2 = e by A1,MSUALG_2:def 13;
   hence thesis;
 end;
end;

:: maybe do another definition of ossort, saying that it contains
:: Elements of subsort which are order-sorted (or ossubsets)
theorem Th24:
  for A,B be OSSubset of OU0 holds
  B in OSSubSort(A) iff B is opers_closed &
  OSConstants(OU0) c= B & A c= B
 proof let A, B be OSSubset of OU0;
  A1: B is OrderSortedSet of S1 by Def2;
  thus B in OSSubSort(A) implies
  B is opers_closed & OSConstants(OU0) c= B & A c= B
  proof assume B in OSSubSort(A);
    then B in
    { x where x is Element of SubSort(A): x is OrderSortedSet of S1}
    by Def7;
    then consider B1 being Element of SubSort(A) such that
    A2: B1 = B & B1 is OrderSortedSet of S1;
      B is opers_closed & Constants(OU0) c= B & A c= B
    by A2,MSUALG_2:14;
    hence thesis by Th16;
  end;
  assume A3: B is opers_closed & OSConstants(OU0) c= B & A c= B;
    Constants(OU0) c= OSConstants(OU0) by Th15;
  then Constants(OU0) c= B by A3,PBOOLE:15;
  then B in SubSort(A) by A3,MSUALG_2:14;
  then B in
  { x where x is Element of SubSort(A): x is OrderSortedSet of S1} by A1;
  hence thesis by Def7;
end;

theorem Th25:
for B be OSSubset of OU0 holds B in OSSubSort(OU0) iff B is opers_closed
 proof let B be OSSubset of OU0;
   A1: B is OrderSortedSet of S1 by Def2;
   A2: B in SubSort(OU0) iff B is opers_closed by MSUALG_2:15;
   A3: B in OSSubSort(OU0) iff B in
   { x where x is Element of SubSort(OU0): x is OrderSortedSet of S1}
   by Def8;
   thus B in OSSubSort(OU0) implies B is opers_closed
   proof assume B in OSSubSort(OU0);
     then consider B1 being Element of SubSort(OU0) such that A4:
     B1 = B & B1 is OrderSortedSet of S1 by A3;
     thus thesis by A4,MSUALG_2:15;
   end;
   assume B is opers_closed;
   hence B in OSSubSort(OU0) by A1,A2,A3;
end;

:: slices of members of OSsubsort
definition let S1,OU0;
           let A be OSSubset of OU0,
               s be Element of S1;
func OSSubSort(A,s) -> set means :Def10:
for x be set holds
 x in it iff ex B be OSSubset of OU0 st B in OSSubSort(A) & x = B.s;
 existence
 proof
   set C =bool Union (the Sorts of OU0);
   A1: C = bool union( rng(the Sorts of OU0)) by PROB_1:def 3;
   defpred P[set] means ex B be OSSubset of OU0 st
   B in OSSubSort(A) & $1 = B.s;
   consider X be set such that
   A2: for x be set holds
   x in X iff x in C & P[x] from Separation;
   A3: for x be set holds
   x in X iff ex B be OSSubset of OU0 st B in OSSubSort(A) & x = B.s
   proof let x be set;
     thus x in X implies
       ex B be OSSubset of OU0 st B in OSSubSort(A) & x = B.s by A2;
     given B be OSSubset of OU0 such that
     A4: B in OSSubSort(A) & x = B.s;
       dom (the Sorts of OU0) = the carrier of S1 &
     dom B = the carrier of S1 by PBOOLE:def 3;
     then (the Sorts of OU0).s in rng (the Sorts of OU0) by FUNCT_1:def 5;
     then A5: (the Sorts of OU0).s c= union( rng (the Sorts of OU0)) by
ZFMISC_1:92;
       B c= the Sorts of OU0 by MSUALG_2:def 1;
     then B.s c= (the Sorts of OU0).s by PBOOLE:def 5;
     then x c= union( rng (the Sorts of OU0)) by A4,A5,XBOOLE_1:1;
     hence thesis by A1,A2,A4;
    end;
   take X;
   thus thesis by A3;
  end;
  uniqueness
  proof
    defpred P[set] means
      ex B be 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 P[x]) &
    (for x being set holds x in X2 iff P[x]) holds X1 = X2 from SetEq;
  end;
end;

theorem Th26:
  for A being OSSubset of OU0,
      s1,s2 being SortSymbol of S1 holds
  s1 <= s2 implies OSSubSort(A,s2) is_coarser_than OSSubSort(A,s1)
proof
  let A be OSSubset of OU0,
  s1,s2 be SortSymbol of S1;
  assume A1: s1 <= s2;
    for Y being set st Y in OSSubSort(A,s2) ex X being set st
  X in OSSubSort(A,s1) & X c= Y
  proof
    let x be set such that A2: x in OSSubSort(A,s2);
    consider B being OSSubset of OU0 such that A3:
    B in OSSubSort(A) & x = B.s2 by A2,Def10;
    A4: B is OrderSortedSet of S1 by Def2;
    take B.s1;
    thus thesis by A1,A3,A4,Def10,OSALG_1:def 18;
  end;
  hence thesis by SETFAM_1:def 3;
end;

theorem Th27:
  for A being OSSubset of OU0, s being SortSymbol of S1 holds
  OSSubSort(A,s) c= SubSort(A,s)
proof
  let A be OSSubset of OU0,
      s be SortSymbol of S1;
  let x be set;
  assume x in OSSubSort(A,s);
  then consider B being OSSubset of OU0 such that A1:
  B in OSSubSort(A) & x = B.s by Def10;
    OSSubSort(A) c= SubSort(A) by Th21;
  hence thesis by A1,MSUALG_2:def 14;
end;

theorem Th28:
  for A being OSSubset of OU0, s being SortSymbol of S1 holds
  (the Sorts of OU0).s in OSSubSort(A,s)
proof
  let A be OSSubset of OU0, s be SortSymbol of S1;
  A1: the Sorts of OU0 in OSSubSort(A) by Th22;
    the Sorts of OU0 is ManySortedSubset of the Sorts of OU0 &
  the Sorts of OU0 is OrderSortedSet of S1
  by MSUALG_2:def 1,OSALG_1:17;
  then reconsider B = the Sorts of OU0 as OSSubset of OU0 by Def2;
    B.s in OSSubSort(A,s) by A1,Def10;
  hence thesis;
end;

definition let S1,OU0;
  let A be OSSubset of OU0,
      s be SortSymbol of S1;
  cluster OSSubSort(A,s) -> non empty;
  coherence by Th28;
end;

definition let S1,OU0;
           let A be OSSubset of OU0;
  func OSMSubSort(A) -> OSSubset of OU0 means :Def11:
  for s be SortSymbol of S1 holds it.s = meet (OSSubSort(A,s));
 existence
 proof
   deffunc F(Element of S1) = meet (OSSubSort(A,$1));
   consider f be Function such that A1: dom f = the carrier of S1 &
   for s be Element of S1
   holds f.s = F(s) from LambdaB;
   reconsider f as ManySortedSet of (the carrier of S1) by A1,PBOOLE:def 3;
     f c= the Sorts of OU0
   proof let x be set;
     assume x in the carrier of S1;
     then reconsider s = x as SortSymbol of S1;
     A2: f.s = meet (OSSubSort(A,s)) by A1;
     reconsider u0 = the Sorts of OU0 as MSSubset of OU0 by MSUALG_2:def 1;
       u0 is OrderSortedSet of S1 by OSALG_1:17;
     then A3: u0 is OSSubset of OU0 by Def2;
       u0 in OSSubSort(A) by Th22;
     then (the Sorts of OU0).s in (OSSubSort(A,s)) by A3,Def10;
     hence thesis by A2,SETFAM_1:4;
   end;
   then reconsider f as MSSubset of OU0 by MSUALG_2:def 1;
   take f;
   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;
     assume A4: s1 <= s2;
     reconsider s3 = s1, s4 = s2 as SortSymbol of S1;
       OSSubSort(A,s4) is_coarser_than OSSubSort(A,s3) by A4,Th26;
     then A5: meet OSSubSort(A,s1) c= meet OSSubSort(A,s2) by SETFAM_1:19;
       f1.s1 = meet OSSubSort(A,s1) by A1;
     hence f1.s1 c= f1.s2 by A1,A5;
   end;
   then f is OrderSortedSet of S1 by OSALG_1:def 18;
   hence thesis by A1,Def2;
  end;
 uniqueness
 proof let W1,W2 be OSSubset of OU0;
   assume A6: (for s be SortSymbol of S1 holds W1.s = meet (OSSubSort(A,s))) &
         (for s be SortSymbol of S1 holds W2.s = meet (OSSubSort(A,s)));
     for s be set st s in (the carrier of S1) holds W1.s = W2.s
   proof let s be set;
     assume s in (the carrier of S1);
     then reconsider s as SortSymbol of S1;
       W1.s = meet (OSSubSort(A,s)) & W2.s = meet (OSSubSort(A,s)) by A6;
     hence thesis;
   end;
   hence thesis by PBOOLE:3;
  end;
end;

definition let S1,OU0;
  canceled;
  cluster opers_closed OSSubset of OU0;
  existence
  proof
    consider x being Element of OSSubSort(OU0);
    x in OSSubSort(OU0);
    then x in
    { y where y is Element of SubSort(OU0): y is OrderSortedSet of S1}
    by Def8;
    then consider x1 being Element of SubSort(OU0) such that A1:
    x = x1 & x1 is OrderSortedSet of S1;
    reconsider x2 = x1 as MSSubset of OU0 by MSUALG_2:def 12;
    A2: x2 is opers_closed by MSUALG_2:def 12;
    reconsider x3 = x2 as OSSubset of OU0 by A1,Def2;
    take x3;
    thus thesis by A2;
  end;
end;

theorem Th29:
for A be OSSubset of OU0 holds OSConstants(OU0) \/ A c= OSMSubSort(A)
 proof let A be OSSubset of OU0;
  let i be set; assume i in the carrier of S1;
  then reconsider s = i as SortSymbol of S1;
  A1: (OSMSubSort(A)).s = meet (OSSubSort(A,s)) by Def11;
    for Z be set st Z in OSSubSort(A,s) holds
  (OSConstants(OU0) \/ A).s c= Z
  proof let Z be set;
    assume Z in OSSubSort(A,s);
    then consider B be OSSubset of OU0 such that
    A2: B in OSSubSort(A) & Z = B.s by Def10;
      OSConstants(OU0) c= B & A c= B by A2,Th24;
    then OSConstants(OU0) \/ A c= B by PBOOLE:18;
    hence thesis by A2,PBOOLE:def 5;
   end;
  hence thesis by A1,SETFAM_1:6;
 end;

theorem
  for A be OSSubset of OU0 st OSConstants(OU0) \/ A is non-empty holds
OSMSubSort(A) is non-empty
 proof let A be OSSubset of OU0;
  assume A1: OSConstants(OU0) \/ A is non-empty;
    now let i be set; assume i in the carrier of S1;
  then reconsider s = i as SortSymbol of S1;
  A2: (OSConstants(OU0) \/ A).s is non empty by A1,PBOOLE:def 16;
    for Z be set st Z in OSSubSort(A,s) holds (OSConstants(OU0) \/ A).s c= Z
   proof let Z be set;
    assume Z in OSSubSort(A,s);
    then consider B be OSSubset of OU0 such that
    A3: B in OSSubSort(A) & Z = B.s by Def10;
      OSConstants(OU0) c= B & A c= B by A3,Th24;
    then OSConstants(OU0) \/ A c= B by PBOOLE:18;
    hence thesis by A3,PBOOLE:def 5;
   end;
  then A4: (OSConstants(OU0) \/ A).s c= meet(OSSubSort(A,s)) by SETFAM_1:6;
  consider x be set such that A5: x in (OSConstants(OU0) \/
 A).s by A2,XBOOLE_0:def 1;
  thus (OSMSubSort(A)).i is non empty by A4,A5,Def11;
 end;
 hence thesis by PBOOLE:def 16;
 end;

theorem Th31:
for o be OperSymbol of S1
for A be OSSubset of OU0
for B be 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 o be OperSymbol of S1,
      A be OSSubset of OU0, B be OSSubset of OU0;
  assume A1: B in OSSubSort(A);
    OSMSubSort (A) c= B
   proof let i be set;
    assume i in the carrier of S1;
    then reconsider s = i as SortSymbol of S1;
    A2: (OSMSubSort A).s = meet (OSSubSort(A,s)) by Def11;
      B.s in (OSSubSort(A,s)) by A1,Def10;
    hence thesis by A2,SETFAM_1:4;
   end;
  hence thesis by MSUALG_2:3;
 end;

theorem Th32:
for o be OperSymbol of S1
for A be OSSubset of OU0
for B be 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 o be OperSymbol of S1;
  let A be OSSubset of OU0, B be OSSubset of OU0;
  set m = ((OSMSubSort A)# * (the Arity of S1)).o,
      b = (B# * (the Arity of S1)).o,
      d = Den(o,OU0);
  assume A1: B in OSSubSort(A);
  then m c= b by Th31;
  then b /\ m = m by XBOOLE_1:28;
  then d|m = (d|b)|m by RELAT_1:100;
  then A2: rng (d|m) c= rng(d|b) by FUNCT_1:76;
    B is opers_closed by A1,Th24;
  then B is_closed_on o by MSUALG_2:def 7;
  then rng (d|b) c= (B * (the ResultSort of S1)).o by MSUALG_2:def 6;
  hence thesis by A2,XBOOLE_1:1;
 end;

theorem Th33:
for o be OperSymbol of S1
for A be 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 o be OperSymbol of S1;
  let A be OSSubset of OU0;
  let x be set; 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;
  set r = the_result_sort_of o;
  A3: r = (the ResultSort of S1).o by MSUALG_1:def 7;
  A4: dom (the ResultSort of S1) = the OperSymbols of S1 &
  rng (the ResultSort of S1) c= the carrier of S1 by FUNCT_2:def 1,RELSET_1:12;
   then ((OSMSubSort A) * (the ResultSort of S1)).o = (OSMSubSort A).r
                                                     by A3,FUNCT_1:23
      .= meet OSSubSort(A,r) by Def11;
  then consider X be set such that
  A5: X in OSSubSort(A,r) & not x in X by A2,SETFAM_1:def 1;
  consider B be OSSubset of OU0 such that
  A6: B in OSSubSort(A) & B.r = X by A5,Def10;
    rng (Den(o,OU0)|(((OSMSubSort A)# * (the Arity of S1)).o)) c=
  (B * (the ResultSort of S1)).o by A6,Th32;
   then x in (B * (the ResultSort of S1)).o by A1;
  hence contradiction by A3,A4,A5,A6,FUNCT_1:23;
 end;

theorem Th34:
for A be OSSubset of OU0 holds
OSMSubSort(A) is opers_closed & A c= OSMSubSort(A)
 proof let A be OSSubset of OU0;
  thus OSMSubSort(A) is opers_closed
   proof let o1 be Element of the OperSymbols of S1;
     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 Th33;
    hence thesis by MSUALG_2:def 6;
   end;
  A1: A c= OSConstants(OU0) \/ A by PBOOLE:16;
    OSConstants(OU0) \/ A c= OSMSubSort(A) by Th29;
  hence thesis by A1,PBOOLE:15;
 end;

definition
  let S1,OU0;
  let A be OSSubset of OU0;
  cluster OSMSubSort(A) -> opers_closed;
  coherence by Th34;
end;

begin :: Operations on Subalgebras of an Order Sorted Algebra.

definition let S1,OU0;
  let A be opers_closed OSSubset of OU0;
  cluster OU0|A -> order-sorted;
  coherence
  proof
    set M = MSAlgebra (#A, Opers(OU0,A) qua ManySortedFunction of
                      (A# * the Arity of S1),(A * the ResultSort of S1)#);
    A1: OU0|A = M by MSUALG_2:def 16;
      A is OrderSortedSet of S1 by Def2;
    hence thesis by A1,OSALG_1:17;
  end;
end;

definition let S1,OU0;
           let OU1,OU2 be OSSubAlgebra of OU0;
cluster OU1 /\ OU2 -> order-sorted;
coherence
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 17;
  hence OU1 /\ OU2 is order-sorted by OSALG_1:17;
end;
end;

:: generally, GenOSAlg can differ from GenMSAlg, example should be given
definition
  let S1,OU0;
  let A be OSSubset of OU0;
func GenOSAlg(A) -> strict OSSubAlgebra of OU0 means :Def13:
 A is OSSubset of it &
 for OU1 be OSSubAlgebra of OU0 st A is OSSubset of OU1 holds
       it is OSSubAlgebra of OU1;
 existence
 proof
   A1: A is OrderSortedSet of S1 by Def2;
   set a = OSMSubSort(A);
   A2: a is opers_closed & A c= a by Th34;
   reconsider u1 = OU0|a as strict OSSubAlgebra of OU0;
   take u1;
   A3: u1 = MSAlgebra (# a, Opers(OU0,a)qua ManySortedFunction of
                (a# * the Arity of S1),(a * the ResultSort of S1)#)
                by MSUALG_2:def 16;
   then A is MSSubset of u1 by A2,MSUALG_2:def 1;
   hence A is OSSubset of u1 by A1,Def2;
   let U2 be OSSubAlgebra of OU0;
   reconsider B1 = the Sorts of U2 as MSSubset of OU0
   by MSUALG_2:def 10;
     B1 is OrderSortedSet of S1 by OSALG_1:17;
   then reconsider B = B1 as OSSubset of OU0 by Def2;
   A4: B is opers_closed by MSUALG_2:def 10;
   assume A is OSSubset of U2;
   then A5: A c= B by MSUALG_2:def 1;
     OSConstants(OU0) is OSSubset of U2 by Th18;
   then OSConstants(OU0) c= B by MSUALG_2:def 1;
   then A6: B in OSSubSort(A) by A4,A5,Th24;
     the Sorts of u1 c= the Sorts of U2
    proof let i be set;
     assume i in the carrier of S1;
     then reconsider s = i as SortSymbol of S1;
     A7: (the Sorts of u1).s = meet OSSubSort(A,s)
     by A3,Def11;
       B.s in OSSubSort(A,s) by A6,Def10;
     hence thesis by A7,SETFAM_1:4;
    end;
   hence u1 is OSSubAlgebra of U2 by MSUALG_2:9;
  end;
 uniqueness
 proof let W1,W2 be strict OSSubAlgebra of OU0;
   assume
     A is OSSubset of W1 &
   (for U1 be OSSubAlgebra of OU0 st A is OSSubset of U1 holds
   W1 is OSSubAlgebra of U1) &
    A is OSSubset of W2 &
   (for U2 be OSSubAlgebra of OU0 st A is OSSubset of U2 holds
   W2 is OSSubAlgebra of U2);
   then W1 is strict OSSubAlgebra of W2 & W2 is strict OSSubAlgebra of W1;
  hence thesis by MSUALG_2:8;
 end;
end;

:: this should rather be a definition, but I want to keep
:: compatibility of the definition with MSUALG_2
theorem Th35:
  for A be OSSubset of OU0 holds
  GenOSAlg(A) = OU0 | OSMSubSort(A) &
  the Sorts of GenOSAlg(A) = OSMSubSort(A)
proof
  let A be OSSubset of OU0;
   A1: A is OrderSortedSet of S1 by Def2;
   set a = OSMSubSort(A);
   A2: a is opers_closed & A c= a by Th34;
   reconsider u1 = OU0|a as strict OSSubAlgebra of OU0;
   A3: u1 = MSAlgebra (# a, Opers(OU0,a)qua ManySortedFunction of
                (a# * the Arity of S1),(a * the ResultSort of S1)#)
                by MSUALG_2:def 16;
   A4: A is OSSubset of u1 &
   for OU1 be OSSubAlgebra of OU0 st A is OSSubset of OU1 holds
       u1 is OSSubAlgebra of OU1
   proof
       A is MSSubset of u1 by A2,A3,MSUALG_2:def 1;
     hence A is OSSubset of u1 by A1,Def2;
     let U2 be OSSubAlgebra of OU0;
     reconsider B1 = the Sorts of U2 as MSSubset of OU0
     by MSUALG_2:def 10;
       B1 is OrderSortedSet of S1 by OSALG_1:17;
     then reconsider B = B1 as OSSubset of OU0 by Def2;
     A5: B is opers_closed by MSUALG_2:def 10;
     assume A is OSSubset of U2;
     then A6: A c= B by MSUALG_2:def 1;
       OSConstants(OU0) is OSSubset of U2 by Th18;
     then OSConstants(OU0) c= B by MSUALG_2:def 1;
     then A7: B in OSSubSort(A) by A5,A6,Th24;
       the Sorts of u1 c= the Sorts of U2
     proof let i be set;
       assume i in the carrier of S1;
       then reconsider s = i as SortSymbol of S1;
       A8: (the Sorts of u1).s = meet OSSubSort(A,s)
       by A3,Def11;
         B.s in OSSubSort(A,s) by A7,Def10;
       hence thesis by A8,SETFAM_1:4;
     end;
     hence u1 is OSSubAlgebra of U2 by MSUALG_2:9;
   end;
   hence GenOSAlg(A) = OU0|a by Def13;
   thus thesis by A3,A4,Def13;
end;

:: this could simplify some proofs in MSUALG_2, I need it anyway
theorem Th36:
 for S be non void non empty ManySortedSign
 for U0 be MSAlgebra over S
 for A be MSSubset of U0 holds
  GenMSAlg(A) = U0 | MSSubSort(A) &
  the Sorts of GenMSAlg(A) = MSSubSort(A)
proof
  let S be non void non empty ManySortedSign,
      U0 be MSAlgebra over S,
      A be MSSubset of U0;
  set a = MSSubSort(A);
  A1: a is opers_closed & A c= a by MSUALG_2:21;
  reconsider u1 = U0|a as strict MSSubAlgebra of U0;
  A2: u1 = MSAlgebra (# a, Opers(U0,a)qua ManySortedFunction of
                (a# * the Arity of S),(a * the ResultSort of S)#)
                by A1,MSUALG_2:def 16;
   A3: A is MSSubset of u1 &
   for U1 be MSSubAlgebra of U0 st A is MSSubset of U1 holds
       u1 is MSSubAlgebra of U1
   proof
   thus A is MSSubset of u1 by A1,A2,MSUALG_2:def 1;
   let U2 be MSSubAlgebra of U0;
   reconsider B = the Sorts of U2 as MSSubset of U0 by MSUALG_2:def 10;
   A4: B is opers_closed by MSUALG_2:def 10;
   assume A is MSSubset of U2;
   then A5: A c= B by MSUALG_2:def 1;
     Constants(U0) is MSSubset of U2 by MSUALG_2:11;
   then Constants(U0) c= B by MSUALG_2:def 1;
   then A6: B in SubSort(A) by A4,A5,MSUALG_2:14;
     the Sorts of u1 c= the Sorts of U2
    proof let i be set;
     assume i in the carrier of S;
     then reconsider s = i as SortSymbol of S;
     A7: (the Sorts of u1).s = meet SubSort(A,s)
     by A2,MSUALG_2:def 15;
       B.s in SubSort(A,s) by A6,MSUALG_2:def 14;
     hence thesis by A7,SETFAM_1:4;
    end;
   hence u1 is MSSubAlgebra of U2 by MSUALG_2:9;
 end;
 hence GenMSAlg(A) = U0|a by MSUALG_2:def 18;
 thus thesis by A2,A3,MSUALG_2:def 18;
end;

theorem Th37:
  for A being OSSubset of OU0 holds
  the Sorts of GenMSAlg(A) c= the Sorts of GenOSAlg(A)
proof
  let A be OSSubset of OU0;
  set GM = GenMSAlg(A), GO = GenOSAlg(A);
  A1: the Sorts of GM = MSSubSort(A) &
      the Sorts of GO = OSMSubSort(A) by Th35,Th36;
  let i be set;
  assume i in the carrier of S1;
  then reconsider s = i as SortSymbol of S1;
  A2: (the Sorts of GO).s = meet OSSubSort(A,s)
  by A1,Def11;
  A3: (the Sorts of GM).s = meet SubSort(A,s)
  by A1,MSUALG_2:def 15;
    OSSubSort(A,s) c= SubSort(A,s) by Th27;
  hence (the Sorts of GM).i c= (the Sorts of GO).i by A2,A3,SETFAM_1:7;
end;

theorem Th38:
  for A being OSSubset of OU0 holds
  GenMSAlg(A) is MSSubAlgebra of GenOSAlg(A)
proof
  let A be OSSubset of OU0;
    the Sorts of GenMSAlg(A) c= the Sorts of GenOSAlg(A) by Th37;
  hence thesis by MSUALG_2:9;
end;

theorem Th39:
  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 OU0 be strict OSAlgebra of S1;
  let B be OSSubset of OU0;
  assume B = the Sorts of OU0;
  then A1: GenMSAlg(B) = OU0 by MSUALG_2:22;
    GenMSAlg(B) is strict MSSubAlgebra of GenOSAlg(B) by Th38;
  hence thesis by A1,MSUALG_2:8;
end;

theorem Th40:
  for OU1 being strict OSSubAlgebra of OU0,
      B being OSSubset of OU0 st B = the Sorts of OU1
  holds GenOSAlg(B) = OU1
proof
  let OU1 be strict OSSubAlgebra of OU0;
  let B be OSSubset of OU0;
  A1: B is OrderSortedSet of S1 by Def2;
  assume A2: B = the Sorts of OU1;
  then B is MSSubset of OU1 by MSUALG_2:def 1;
  then A3: B is OSSubset of OU1 by A1,Def2;
  set W = GenOSAlg(B);
  A4: B is OSSubset of W by Def13;
  A5: W is strict OSSubAlgebra of OU1 by A3,Def13;
    the Sorts of OU1 c= the Sorts of W by A2,A4,MSUALG_2:def 1;
  then OU1 is strict MSSubAlgebra of W by MSUALG_2:9;
  hence thesis by A5,MSUALG_2:8;
end;

theorem Th41:
 for U0 be non-empty OSAlgebra of S1,
     U1 be OSSubAlgebra of U0 holds
GenOSAlg(OSConstants(U0)) /\ U1 = GenOSAlg(OSConstants(U0))
 proof let U0 be non-empty OSAlgebra of S1,
           U1 be OSSubAlgebra of U0;
  set C = OSConstants(U0),
      G = GenOSAlg(C);
  A1: the Sorts of ( G /\ U1) = (the Sorts of G) /\ (the Sorts of U1)
  by MSUALG_2:def 17;
    C is OSSubset of U1 by Th18;
  then G is strict OSSubAlgebra of U1 by Def13;
  then the Sorts of G is MSSubset of U1 & the Sorts of G
  is OrderSortedSet of S1 by MSUALG_2:def 10,OSALG_1:17;
  then the Sorts of G c= the Sorts of U1 by MSUALG_2:def 1;
  then the Sorts of ( G /\ U1) = the Sorts of G by A1,PBOOLE:25;
 hence thesis by MSUALG_2:10;
 end;

definition let S1;
           let U0 be non-empty OSAlgebra of S1,
               U1,U2 be OSSubAlgebra of U0;
func U1 "\/"_os U2 -> strict OSSubAlgebra of U0 means :Def14:
 for A be OSSubset of U0 st
  A = (the Sorts of U1) \/ (the Sorts of U2) holds it = GenOSAlg(A);
  existence
   proof
    set B=(the Sorts of U1) \/ (the Sorts of U2);
       the Sorts of U1 is MSSubset of U0 &
    the Sorts of U2 is MSSubset of U0 by MSUALG_2:def 10;
    then the Sorts of U1 c=the Sorts of U0 &
    the Sorts of U2 c=the Sorts of U0 by MSUALG_2:def 1;
    then B c= the Sorts of U0 by PBOOLE:18;
    then reconsider B as MSSubset of U0 by MSUALG_2:def 1;
    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);
    thus thesis;
   end;
  uniqueness
   proof let W1,W2 be strict OSSubAlgebra of U0;
    assume A1:(for A be OSSubset of U0 st
    A = (the Sorts of U1) \/ (the Sorts of U2) holds W1 = GenOSAlg(A)) &
    ( for A be OSSubset of U0 st
    A = (the Sorts of U1) \/ (the Sorts of U2) holds W2 = GenOSAlg(A));
    set B=(the Sorts of U1) \/ (the Sorts of U2);
       the Sorts of U1 is MSSubset of U0 &
    the Sorts of U2 is MSSubset of U0 by MSUALG_2:def 10;
    then the Sorts of U1 c=the Sorts of U0 &
    the Sorts of U2 c=the Sorts of U0 by MSUALG_2:def 1;
    then B c= the Sorts of U0 by PBOOLE:18;
    then reconsider B as MSSubset of U0 by MSUALG_2:def 1;
    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;
      W1 = GenOSAlg(B0) & W2 = GenOSAlg(B0) by A1;
   hence thesis;
  end;
end;

theorem Th42:
  for U0 be non-empty OSAlgebra of S1,
  U1 be OSSubAlgebra of U0, A,B be OSSubset of U0
  st B = A \/ the Sorts of U1
  holds GenOSAlg(A) "\/"_os U1 = GenOSAlg(B)
proof let U0 be non-empty OSAlgebra of S1,
           U1 be OSSubAlgebra of U0,
           A,B be OSSubset of U0;
  A1: A is OrderSortedSet of S1 & B is OrderSortedSet of S1
  by Def2;
  assume A2: B = A \/ the Sorts of U1;
    A is OSSubset of GenOSAlg(A) by Def13;
  then A3:A c= the Sorts of GenOSAlg(A) by MSUALG_2:def 1;
  reconsider u1m = the Sorts of U1, am = the Sorts of GenOSAlg(A)
             as MSSubset of U0 by MSUALG_2:def 10;
  A4: 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 MSUALG_2:def 1;
   then a \/ u1 c= the Sorts of U0 by PBOOLE:18;
  then reconsider b=a \/ u1 as MSSubset of U0 by MSUALG_2:def 1;
  A5: a \/ u1 is OrderSortedSet of S1 by A4,Th2;
  then reconsider b as OSSubset of U0 by Def2;
  A6: (GenOSAlg(A) "\/"_os U1) = GenOSAlg(b) by Def14;
  then a \/ u1 is OSSubset of (GenOSAlg(A)"\/"_os U1) by Def13;
  then A7: a \/ u1 c=the Sorts of (GenOSAlg(A)"\/"_os U1) by MSUALG_2:def 1;
    A \/ u1 c= a \/ u1 by A3,PBOOLE:22;
  then B c=the Sorts of (GenOSAlg(A)"\/"_os U1) by A2,A7,PBOOLE:15;
  then B is MSSubset of (GenOSAlg(A)"\/"_os U1) by MSUALG_2:def 1;
  then B is OSSubset of (GenOSAlg(A)"\/"_os U1) by A1,Def2;
  then A8:GenOSAlg(B) is strict OSSubAlgebra of (GenOSAlg(A)"\/"_os U1)
  by Def13;
    B is OSSubset of GenOSAlg(B) & u1 c= B & A c= B by A2,Def13,PBOOLE:16;
  then B c= the Sorts of GenOSAlg(B) & u1 c= B & A c= B by MSUALG_2:def 1;
  then A9: u1 c= the Sorts of GenOSAlg(B) & A c= the Sorts of GenOSAlg(B)
                                                    by PBOOLE:15;
  then A10: A c= (the Sorts of GenOSAlg(A)) /\ (the Sorts of GenOSAlg(B))
                                                    by A3,PBOOLE:19;
  A11:the Sorts of (GenOSAlg(A) /\ GenOSAlg(B)) =
          (the Sorts of GenOSAlg(A)) /\
 (the Sorts of GenOSAlg(B)) by MSUALG_2:def 17;
  then A is MSSubset of (GenOSAlg(A) /\ GenOSAlg(B)) by A10,MSUALG_2:def 1;
  then A is OSSubset of (GenOSAlg(A) /\ GenOSAlg(B)) by A1,Def2;
  then GenOSAlg(A) is OSSubAlgebra of (GenOSAlg(A) /\ GenOSAlg(B)) by Def13;
  then a is MSSubset of (GenOSAlg(A) /\ GenOSAlg(B)) by MSUALG_2:def 10;
  then A12:a c= (the Sorts of GenOSAlg(A)) /\ (the Sorts of GenOSAlg(B))
  by A11,MSUALG_2:def 1;
    (the Sorts of GenOSAlg(A)) /\ (the Sorts of GenOSAlg(B)) c= a
  by PBOOLE:17;
  then a= (the Sorts of GenOSAlg(A)) /\ (the Sorts of GenOSAlg(B))
  by A12,PBOOLE:def 13;
  then a c= the Sorts of GenOSAlg(B) by PBOOLE:17;
  then b c= the Sorts of GenOSAlg(B) by A9,PBOOLE:18;
  then b is MSSubset of GenOSAlg(B) by MSUALG_2:def 1;
  then b is OSSubset of GenOSAlg(B) by A5,Def2;
  then GenOSAlg(b) is strict OSSubAlgebra of GenOSAlg(B) by Def13;
 hence thesis by A6,A8,MSUALG_2:8;
 end;

theorem Th43:
  for U0 be non-empty OSAlgebra of S1,
  U1 be OSSubAlgebra of U0, B be OSSubset of U0
  st B = the Sorts of U0
  holds GenOSAlg(B) "\/"_os U1 = GenOSAlg(B)
proof let U0 be non-empty OSAlgebra of S1,
            U1 be OSSubAlgebra of U0,
            B be OSSubset of U0;
  assume A1: B = the Sorts of U0;
    the Sorts of U1 is MSSubset of U0 by MSUALG_2:def 10;
  then the Sorts of U1 c= B by A1,MSUALG_2:def 1;
  then B \/ the Sorts of U1 = B by PBOOLE:24;
 hence thesis by Th42;
end;

theorem Th44:
for U0 being non-empty OSAlgebra of S1,
U1,U2 be OSSubAlgebra of U0 holds
U1 "\/"_os U2 = U2 "\/"_os U1
 proof let U0 be non-empty OSAlgebra of S1,
           U1,U2 be OSSubAlgebra of U0;
  reconsider u1= the Sorts of U1, u2= the Sorts of U2
              as MSSubset of U0 by MSUALG_2:def 10;
  A1:
  u1 is OrderSortedSet of S1 & u2 is OrderSortedSet of S1 by OSALG_1:17;
    u1 c= the Sorts of U0 & u2 c= the Sorts of U0 by MSUALG_2:def 1;
  then u1 \/ u2 c= the Sorts of U0 by PBOOLE:18;
  then reconsider A1 = u1 \/ u2 as MSSubset of U0 by MSUALG_2:def 1;
    A1 is OrderSortedSet of S1 by A1,Th2;
  then reconsider A = A1 as OSSubset of U0 by Def2;
    U1 "\/"_os U2 = GenOSAlg(A) by Def14;
  hence thesis by Def14;
 end;

theorem Th45:
  for U0 be non-empty OSAlgebra of S1,
  U1,U2 be strict OSSubAlgebra of U0 holds
  U1 /\ (U1"\/"_os U2) = U1
proof let U0 be non-empty OSAlgebra of S1,
           U1,U2 be strict OSSubAlgebra of U0;
  reconsider u1= the Sorts of U1 ,u2 =the Sorts of U2
  as MSSubset of U0 by MSUALG_2:def 10;
  A1: u1 is OrderSortedSet of S1 & u2 is OrderSortedSet of S1
  by OSALG_1:17;
    u1 c= the Sorts of U0 & u2 c= the Sorts of U0 by MSUALG_2:def 1;
  then u1 \/ u2 c= the Sorts of U0 by PBOOLE:18;
  then reconsider A= u1 \/ u2 as MSSubset of U0 by MSUALG_2:def 1;
    A is OrderSortedSet of S1 by A1,Th2;
  then reconsider A as OSSubset of U0 by Def2;
    U1"\/"_os U2 = GenOSAlg(A) by Def14;
  then A is OSSubset of U1"\/"_os U2 by Def13;
  then A2:A c= the Sorts of (U1 "\/"_os U2) by MSUALG_2:def 1;
    the Sorts of U1 c= A by PBOOLE:16;
  then A3: the Sorts of U1 c= the Sorts of (U1"\/"_os U2) by A2,PBOOLE:15;
  A4:the Sorts of (U1 /\(U1"\/"_os U2))=
  (the Sorts of U1)/\(the Sorts of(U1"\/"_os U2)) by MSUALG_2:def 17;
  then A5:the Sorts of U1 c=the Sorts of (U1 /\(U1"\/"_os U2))
  by A3,PBOOLE:19;
    the Sorts of (U1 /\(U1"\/"_os U2)) c= the Sorts of U1 by A4,PBOOLE:17;
  then A6:the Sorts of (U1 /\(U1"\/"_os U2)) = the Sorts of U1 by A5,PBOOLE:def
13;
  reconsider u112=the Sorts of(U1 /\ (U1"\/"_os U2)) as MSSubset of U0
  by MSUALG_2:def 10;
    u112 is opers_closed & the Charact of (U1/\(U1"\/"_os
  U2))=Opers(U0,u112) by MSUALG_2:def 17;
  hence thesis by A6,MSUALG_2:def 10;
end;

theorem Th46:
  for U0 be non-empty OSAlgebra of S1,
  U1,U2 be strict OSSubAlgebra of U0
  holds (U1 /\ U2) "\/"_os U2 = U2
proof let U0 be non-empty OSAlgebra of S1,
          U1,U2 be strict OSSubAlgebra of U0;
  reconsider u12= the Sorts of (U1 /\ U2), u2 = the Sorts of U2
  as MSSubset of U0 by MSUALG_2:def 10;
  A1: u12 is OrderSortedSet of S1 & u2 is OrderSortedSet of S1
  by OSALG_1:17;
  then reconsider u12, u2 as OSSubset of U0 by Def2;
    u12 c= the Sorts of U0 & u2 c= the Sorts of U0 by MSUALG_2:def 1;
  then u12 \/ u2 c= the Sorts of U0 by PBOOLE:18;
  then reconsider A= u12 \/ u2 as MSSubset of U0 by MSUALG_2:def 1;
    A is OrderSortedSet of S1 by A1,Th2;
  then reconsider A= u12 \/ u2 as OSSubset of U0 by Def2;
  A2:(U1 /\ U2) "\/"_os U2 = GenOSAlg(A) by Def14;
    u12 = (the Sorts of U1) /\ (the Sorts of U2) by MSUALG_2:def 17;
  then u12 c= u2 by PBOOLE:17;
   then A = u2 by PBOOLE:24;
 hence thesis by A2,Th40;
 end;

begin :: The Lattice of SubAlgebras of an Order Sorted Algebra.

:: ossub, ossubalgebra
definition let S1,OU0;
func OSSub(OU0) -> set means :Def15:
for x holds x in it iff x is strict OSSubAlgebra of OU0;
existence
  proof
  set X = {GenOSAlg(@A) where A is Element of OSSubSort(OU0):
     not contradiction};
   take X;
   let x;
   thus x in X implies x is strict OSSubAlgebra of OU0
    proof assume x in X;
     then consider A be Element of OSSubSort(OU0) such that
     A1: x = GenOSAlg(@A);
     thus thesis by A1;
    end;
   assume x is strict OSSubAlgebra of OU0;
   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 Th25;
     @h =A by Def9;
   then a = GenOSAlg(@h) by Th40;
   hence x in X;
  end;
  uniqueness
  proof
    defpred P[set] means $1 is strict OSSubAlgebra of OU0;
    thus for X1,X2 being set st
    (for x being set holds x in X1 iff P[x]) &
    (for x being set holds x in X2 iff P[x]) holds X1 = X2 from SetEq;
  end;
end;

theorem Th47:
  OSSub(OU0) c= MSSub(OU0)
proof
  let x be set such that A1: x in OSSub(OU0);
    x is strict MSSubAlgebra of OU0 by A1,Def15;
  hence thesis by MSUALG_2:def 20;
end;

definition let S be OrderSortedSign,
               U0 be OSAlgebra of S;
cluster OSSub(U0) -> non empty;
 coherence
  proof
    consider x being strict OSSubAlgebra of U0;
      x in OSSub U0 by Def15;
    hence thesis;
  end;
end;

definition let S1,OU0;
  redefine func OSSub(OU0) -> Subset of MSSub(OU0);
  coherence by Th47;
end;

:: maybe show that e.g. for TrivialOSA(S,z,z1), OSSub(U0) is
:: proper subset of MSSub(U0), to have some counterexamples
definition let S1;
           let U0 be non-empty OSAlgebra of S1;
func OSAlg_join(U0) -> BinOp of (OSSub(U0)) means :Def16:
for x,y be Element of OSSub(U0) holds
 for U1,U2 be strict OSSubAlgebra of U0 st x = U1 & y = U2 holds
  it.(x,y) = U1 "\/"_os U2;
  existence
   proof
    defpred P[(Element of OSSub(U0)),(Element of OSSub(U0)),
    Element of OSSub(U0)] means
    for U1,U2 be 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 P[x,y,z]
     proof let x,y be Element of OSSub(U0);
      reconsider U1=x, U2=y as strict OSSubAlgebra of U0 by Def15;
      reconsider z =U1"\/"_os U2 as Element of OSSub(U0)
      by Def15;
      take z;
      thus thesis;
     end;
    consider o be BinOp of OSSub(U0) such that
    A2:for a,b be Element of OSSub(U0) holds P[a,b,o.(a,b)]
    from BinOpEx(A1);
    take o;
    thus thesis by A2;
   end;
  uniqueness
  proof let o1,o2 be BinOp of (OSSub(U0));
    assume A3:(for x,y be Element of OSSub(U0) holds
    for U1,U2 be strict OSSubAlgebra of U0 st x=U1 & y=U2
    holds o1.(x,y)=U1 "\/"_os U2)
    & (for x,y be Element of OSSub(U0) holds
    for U1,U2 be strict OSSubAlgebra of U0 st x=U1 & y=U2 holds
    o2.(x,y) = U1 "\/"_os U2);
      for x be Element of OSSub(U0) for y be Element of OSSub(U0) holds
    o1.(x,y) = o2.(x,y)
    proof let x,y be Element of OSSub(U0);
     reconsider U1=x,U2=y as strict OSSubAlgebra of U0 by Def15;
       o1.(x,y) = U1"\/"_os U2 & o2.(x,y) = U1"\/"_os U2 by A3;
     hence thesis;
    end;
    hence thesis by BINOP_1:2;
   end;
end;

definition let S1;
           let U0 be non-empty OSAlgebra of S1;
func OSAlg_meet(U0) -> BinOp of (OSSub(U0)) means :Def17:
for x,y be Element of OSSub(U0) holds
  for U1,U2 be strict OSSubAlgebra of U0 st x = U1 & y = U2 holds
  it.(x,y) = U1 /\ U2;
  existence
   proof
    defpred P[(Element of OSSub(U0)),(Element of OSSub(U0)),
    Element of OSSub(U0)] means
    for U1,U2 be 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 P[x,y,z]
     proof let x,y be Element of OSSub(U0);
      reconsider U1=x, U2=y as strict OSSubAlgebra of U0 by Def15;
      reconsider z =U1 /\ U2 as Element of OSSub(U0) by Def15;
      take z;
      thus thesis;
     end;
    consider o be BinOp of OSSub(U0) such that
    A2:for a,b be Element of OSSub(U0) holds P[a,b,o.(a,b)] from BinOpEx(A1);
    take o;
    thus thesis by A2;
   end;
  uniqueness
   proof let o1,o2 be BinOp of OSSub(U0);
    assume A3:(for x,y be Element of OSSub(U0) holds
    for U1,U2 be strict OSSubAlgebra of U0 st x=U1 & y=U2
    holds o1.(x,y)=U1 /\ U2)
    & (for x,y be Element of OSSub(U0) holds
    for U1,U2 be strict OSSubAlgebra of U0 st x=U1 & y=U2 holds
    o2.(x,y) = U1 /\ U2);
      for x be Element of OSSub(U0) for y be Element of OSSub(U0) holds
    o1.(x,y) = o2.(x,y)
     proof let x,y be Element of OSSub(U0);
      reconsider U1=x,U2=y as strict OSSubAlgebra of U0 by Def15;
        o1.(x,y) = U1 /\ U2 & o2.(x,y) = U1 /\ U2 by A3;
     hence thesis;
    end;
    hence thesis by BINOP_1:2;
   end;
end;

theorem Th48:
  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 U0 be non-empty OSAlgebra of S1;
  let x,y be Element of OSSub(U0);
    x is strict OSSubAlgebra of U0 &
  y is strict OSSubAlgebra of U0 by Def15;
  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,Def17 .=
  (MSAlg_meet(U0)).(x,y) by A1,MSUALG_2:def 22;
  hence thesis;
end;

reserve U0 for non-empty OSAlgebra of S1;

theorem Th49:
OSAlg_join(U0) is commutative
 proof
  set o = OSAlg_join(U0);
    for x,y be Element of OSSub(U0) holds o.(x,y)=o.(y,x)
   proof let x,y be Element of OSSub(U0);
    reconsider U1=x,U2=y as strict OSSubAlgebra of U0 by Def15;
    A1:o.(x,y) = U1 "\/"_os U2 & o.(y,x) = U2 "\/"_os U1 by Def16;
    set B=(the Sorts of U1) \/ (the Sorts of U2);
      the Sorts of U1 is OrderSortedSet of S1 &
    the Sorts of U2 is OrderSortedSet of S1 by OSALG_1:17;
    then A2: B is OrderSortedSet of S1 by Th2;
      the Sorts of U1 is MSSubset of U0 &
    the Sorts of U2 is MSSubset of U0 by MSUALG_2:def 10;
    then the Sorts of U1 c=the Sorts of U0 &
    the Sorts of U2 c=the Sorts of U0 by MSUALG_2:def 1;
    then B c= the Sorts of U0 by PBOOLE:18;
    then B is MSSubset of U0 by MSUALG_2:def 1;
    then reconsider B as OSSubset of U0 by A2,Def2;
      U1 "\/"_os U2 = GenOSAlg(B) & U2 "\/"_os U1 = GenOSAlg(B)
    by Def14;
   hence thesis by A1;
   end;
  hence thesis by BINOP_1:def 2;
 end;

theorem Th50:
OSAlg_join(U0) is associative
 proof
  set o = OSAlg_join(U0);
    for x,y,z be Element of OSSub(U0) holds o.(x,o.(y,z))=o.(o.(x,y),z)
    proof let x,y,z be Element of OSSub(U0);
    reconsider U1=x,U2=y,U3=z as strict OSSubAlgebra of U0 by Def15;
      o.(y,z)=U2"\/"_os U3 & o.(x,y)=U1"\/"_os U2 by Def16;
    then A1:o.(x,o.(y,z)) = U1 "\/"_os (U2"\/"_os U3) &
    o.(o.(x,y),z) = (U1"\/"_os U2)"\/"_os U3 by Def16;
    set B=(the Sorts of U1) \/ ((the Sorts of U2) \/ (the Sorts of U3));
    A2: (the Sorts of U1) is OrderSortedSet of S1 & (the Sorts of U2) is
    OrderSortedSet of S1 & (the Sorts of U3) is OrderSortedSet of S1
    by OSALG_1:17; then A3:
    (the Sorts of U1) \/ (the Sorts of U2) is OrderSortedSet of S1 &
    (the Sorts of U2) \/ (the Sorts of U3) is OrderSortedSet of S1
    by Th2;
    then A4: B is OrderSortedSet of S1 by A2,Th2;
      the Sorts of U1 is MSSubset of U0 & the Sorts of U2 is MSSubset of U0 &
    the Sorts of U3 is MSSubset of U0 by MSUALG_2:def 10;
    then A5:the Sorts of U1 c=the Sorts of U0 &
      the Sorts of U2 c=the Sorts of U0 &
      the Sorts of U3 c=the Sorts of U0 by MSUALG_2:def 1;
   then A6:(the Sorts of U2) \/ (the Sorts of U3) c= the Sorts of U0
   by PBOOLE:18;
   A7:(the Sorts of U1) \/ (the Sorts of U2) c= the Sorts of U0
   by A5,PBOOLE:18;
   reconsider C1 =(the Sorts of U2) \/ (the Sorts of U3)
   as MSSubset of U0 by A6,MSUALG_2:def 1;
   reconsider C = C1 as OSSubset of U0 by A3,Def2;
   reconsider D1=(the Sorts of U1) \/ (the Sorts of U2)
   as MSSubset of U0 by A7,MSUALG_2:def 1;
   reconsider D = D1 as OSSubset of U0 by A3,Def2;
     B c= the Sorts of U0 by A5,A6,PBOOLE:18;
   then B is MSSubset of U0 by MSUALG_2:def 1;
   then reconsider B as OSSubset of U0 by A4,Def2;
   A8:U1 "\/"_os (U2 "\/"_os U3) = U1 "\/"_os (GenOSAlg(C))
    by Def14 .= (GenOSAlg(C)) "\/"_os U1 by Th44
                 .= GenOSAlg(B) by Th42;
    A9:B= D \/ (the Sorts of U3) by PBOOLE:34;
      (U1"\/"_os U2)"\/"_os U3 = GenOSAlg(D)"\/"_os U3 by Def14
    .= GenOSAlg(B) by A9,Th42;
   hence thesis by A1,A8;
   end;
  hence thesis by BINOP_1:def 3;
 end;

theorem Th51:
  OSAlg_meet(U0) is commutative
proof
  set o = OSAlg_meet(U0);
  set m = MSAlg_meet(U0);
  A1: m is commutative by MSUALG_2:32;
    for x,y be Element of OSSub(U0) holds o.(x,y)=o.(y,x)
  proof let x,y be Element of OSSub(U0);
      o.(x,y) = m.(x,y) by Th48 .= m.(y,x) by A1,BINOP_1:def 2
    .= o.(y,x) by Th48;
    hence thesis;
  end;
  hence thesis by BINOP_1:def 2;
end;

theorem Th52:
  OSAlg_meet(U0) is associative
proof
  set o = OSAlg_meet(U0);
  set m = MSAlg_meet(U0);
  A1: m is associative by MSUALG_2:33;
    for x,y,z be Element of OSSub(U0) holds o.(x,o.(y,z))=o.(o.(x,y),z)
  proof let x,y,z be Element of OSSub(U0);
    A2: o.(y,z) = m.(y,z) & o.(x,y) = m.(x,y) by Th48;
    then o.(x,o.(y,z)) = m.(x,m.(y,z))
    by Th48 .= m.(m.(x,y),z)
    by A1,BINOP_1:def 3 .= o.(o.(x,y),z) by A2,Th48;
    hence thesis;
  end;
  hence thesis by BINOP_1:def 3;
end;

definition let S1;
           let U0 be non-empty OSAlgebra of S1;
func OSSubAlLattice(U0) -> strict Lattice equals :Def18:
  LattStr (# OSSub(U0), OSAlg_join(U0), OSAlg_meet(U0) #);
 coherence
  proof
   set L = LattStr (# OSSub(U0), OSAlg_join(U0), OSAlg_meet(U0) #);
   A1:for a,b being Element of L holds
      (a "\/" b) = (b "\/" a)
    proof let a,b be Element of L;
     reconsider x=a,y=b as Element of OSSub(U0);
     A2:OSAlg_join(U0) is commutative by Th49;
     thus a"\/" b =(OSAlg_join(U0)).(x,y) by LATTICES:def 1
              .= (the L_join of L).(b,a) by A2,BINOP_1:def 2
              .=b"\/" a by LATTICES:def 1;
    end;
   A3:for a,b,c being Element of L
   holds a"\/" (b"\/" c) = (a"\/" b)"\/" c
    proof let a,b,c be Element of L;
     reconsider x=a,y=b,z=c as Element of OSSub(U0);
     A4:OSAlg_join(U0) is associative by Th50;
     thus a"\/" (b"\/" c) = (the L_join of L).(a,(b"\/" c))
     by LATTICES:def 1
     .=(OSAlg_join(U0)).(x,(OSAlg_join(U0)).(y,z)) by LATTICES:def 1
     .= (the L_join of L).((the L_join of L).(a,b),c) by A4,BINOP_1:def 3
     .=((the L_join of L).(a,b))"\/" c by LATTICES:def 1
     .=(a"\/" b)"\/" c by LATTICES:def 1;
    end;
   A5:for a,b being Element of L holds (a"/\"b)"\/" b = b
    proof let a,b be Element of L;
     reconsider x=a,y=b as Element of OSSub(U0);
     A6:(OSAlg_join(U0)).((OSAlg_meet(U0)).(x,y),y)= y
      proof
       reconsider U1= x,U2=y as strict OSSubAlgebra of U0
       by Def15;
         (OSAlg_meet(U0)).(x,y) = U1 /\ U2 by Def17;
       hence (OSAlg_join(U0)).((OSAlg_meet(U0)).(x,y),y)
                             = ((U1 /\ U2)"\/"_os U2) by Def16
                             .=y by Th46;
      end;
     thus (a"/\"b)"\/" b = (the L_join of L).((a"/\"b),b)
     by LATTICES:def 1
              .= b by A6,LATTICES:def 2;
    end;
   A7:for a,b being Element of L holds a"/\"b = b"/\"a
    proof let a,b be Element of L;
     reconsider x=a,y=b as Element of OSSub(U0);
     A8:OSAlg_meet(U0) is commutative by Th51;
     thus a"/\"b =(OSAlg_meet(U0)).(x,y) by LATTICES:def 2
              .= (the L_meet of L).(b,a) by A8,BINOP_1:def 2
              .=b"/\"a by LATTICES:def 2;
    end;
   A9:for a,b,c being Element of L
   holds a"/\"(b"/\"c) = (a"/\"b)"/\"c
    proof let a,b,c be Element of L;
     reconsider x=a,y=b,z=c as Element of OSSub(U0);
     A10:OSAlg_meet(U0) is associative by Th52;
     thus a"/\"(b"/\"c) = (the L_meet of L).(a,(b"/\"c)) by LATTICES:def 2
     .=(OSAlg_meet(U0)).(x,(OSAlg_meet(U0)).(y,z)) by LATTICES:def 2
     .= (the L_meet of L).((the L_meet of L).(a,b),c) by A10,BINOP_1:def 3
     .=((the L_meet of L).(a,b))"/\"c by LATTICES:def 2
     .=(a"/\"b)"/\"c by LATTICES:def 2;
    end;
     for a,b being Element of L holds a"/\"(a"\/" b)=a
   proof let a,b be Element of L;
     reconsider x=a,y=b as Element of OSSub(U0);
     A11:(OSAlg_meet(U0)).(x,(OSAlg_join(U0)).(x,y))= x
      proof
       reconsider U1= x,U2=y as strict OSSubAlgebra of U0 by Def15;
         (OSAlg_join(U0)).(x,y) = U1"\/"_os U2 by Def16;
       hence (OSAlg_meet(U0)).(x,(OSAlg_join(U0)).(x,y))
       = (U1 /\( U1"\/"_os U2)) by Def17
                             .=x by Th45;
      end;
     thus a"/\"(a"\/" b) = (the L_meet of L).(a,(a"\/" b)) by LATTICES:def 2
              .= a by A11,LATTICES:def 1;
    end;
    then L is strict join-commutative join-associative meet-absorbing
      meet-commutative meet-associative join-absorbing
     by A1,A3,A5,A7,A9,LATTICES:def 4,def 5,def 6,def 7,def 8,def 9;
   hence L is strict Lattice by LATTICES:def 10;
  end;
end;

theorem Th53:
  for U0 be non-empty OSAlgebra of S1 holds OSSubAlLattice(U0) is bounded
 proof let U0 be non-empty OSAlgebra of S1;
  set L = OSSubAlLattice(U0);
  A1: L = LattStr (# OSSub(U0), OSAlg_join(U0), OSAlg_meet(U0) #)
  by Def18;
  thus L is lower-bounded
   proof
    set C = OSConstants(U0);
    reconsider G = GenOSAlg(C) as Element of OSSub(U0) by Def15;
    reconsider G1 = G as Element of L by A1;
    take G1;
    let a be Element of L;
    reconsider a1 = a as Element of OSSub(U0) by A1;
    reconsider a2 = a1 as strict OSSubAlgebra of U0 by Def15;
    thus G1 "/\" a =(OSAlg_meet(U0)).(G,a1) by A1,LATTICES:def 2
              .= GenOSAlg(C) /\ a2 by Def17
              .= G1 by Th41;
    hence thesis;
   end;
  thus L is upper-bounded
   proof
    A2: the Sorts of U0 is OrderSortedSet of S1 by OSALG_1:17;
    reconsider B = the Sorts of U0 as MSSubset of U0
    by MSUALG_2:def 1;
    reconsider B as OSSubset of U0 by A2,Def2;
    reconsider G = GenOSAlg(B) as Element of OSSub(U0) by Def15;
    reconsider G1 = G as Element of L by A1;
    take G1;
    let a be Element of L;
    reconsider a1 = a as Element of OSSub(U0) by A1;
    reconsider a2 = a1 as strict OSSubAlgebra of U0 by Def15;
    thus G1"\/" a =(OSAlg_join(U0)).(G1,a) by A1,LATTICES:def 1
              .= GenOSAlg(B)"\/"_os a2 by Def16
              .= G1 by Th43;
    hence thesis;
   end;
 end;

definition let S1;
           let U0 be non-empty OSAlgebra of S1;
cluster OSSubAlLattice(U0) -> bounded;
 coherence by Th53;
end;

theorem
    for U0 be non-empty OSAlgebra of S1
  holds Bottom (OSSubAlLattice(U0)) = GenOSAlg(OSConstants(U0))
 proof let U0 be non-empty OSAlgebra of S1;
  set L = OSSubAlLattice(U0);
  A1: L = LattStr (# OSSub(U0), OSAlg_join(U0), OSAlg_meet(U0) #)
  by Def18;
  set C = OSConstants(U0);
  reconsider G = GenOSAlg(C) as Element of OSSub(U0) by Def15;
  reconsider G1 = G as Element of L by A1;
     now
    let a be Element of L;
    reconsider a1 = a as Element of OSSub(U0) by A1;
    reconsider a2 = a1 as strict OSSubAlgebra of U0 by Def15;
    thus G1 "/\" a =(OSAlg_meet(U0)).(G,a1) by A1,LATTICES:def 2
              .= GenOSAlg(C) /\ a2 by Def17
              .= G1 by Th41;
    hence a "/\" G1 = G1;
   end;
  hence thesis by LATTICES:def 16;
 end;

theorem Th55:
  for U0 be non-empty OSAlgebra of S1,
  B be OSSubset of U0 st B = the Sorts of U0 holds
 Top (OSSubAlLattice(U0)) = GenOSAlg(B)
 proof let U0 be non-empty OSAlgebra of S1, B be OSSubset of U0;
  assume A1: B = the Sorts of U0;
  set L = OSSubAlLattice(U0);
  A2: L = LattStr (# OSSub(U0), OSAlg_join(U0), OSAlg_meet(U0) #)
  by Def18;
  reconsider G = GenOSAlg(B) as Element of OSSub(U0) by Def15;
  reconsider G1 = G as Element of L by A2;
     now
    let a be Element of L;
    reconsider a1 = a as Element of OSSub(U0) by A2;
    reconsider a2 = a1 as strict OSSubAlgebra of U0 by Def15;
    thus G1"\/" a =(OSAlg_join(U0)).(G1,a) by A2,LATTICES:def 1
              .= GenOSAlg(B)"\/"_os a2 by Def16
              .= G1 by A1,Th43;
    hence a "\/" G1 = G1;
   end;
  hence thesis by LATTICES:def 17;
 end;

theorem
    for U0 be strict non-empty OSAlgebra of S1 holds
  Top (OSSubAlLattice(U0)) = U0
 proof let U0 be strict non-empty OSAlgebra of S1;
  reconsider B = the Sorts of U0 as MSSubset of U0 by MSUALG_2:def 1;
    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 Th55
                            .= U0 by Th39;
 end;


Back to top