osalg_2.miz

    begin

    reserve x for set,

R for non empty Poset;

    theorem :: OSALG_2:1



     Th1: for X,Y be 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 s1 <= 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 thesis by A1, XBOOLE_1: 27;

      end;

      hence thesis;

    end;

    theorem :: OSALG_2:2



     Th2: for X,Y be 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 s1 <= 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 thesis by A1, XBOOLE_1: 13;

      end;

      hence thesis;

    end;

    definition

      let R be non empty Poset, M be OrderSortedSet of R;

      :: OSALG_2:def1

      mode OrderSortedSubset of M -> ManySortedSubset of M means

      : Def1: it is OrderSortedSet of R;

      existence

      proof

        reconsider X = M as ManySortedSubset of M by PBOOLE:def 18;

        take X;

        thus thesis;

      end;

    end

    registration

      let R be non empty Poset, M be non-empty OrderSortedSet of R;

      cluster non-empty for OrderSortedSubset of M;

      existence

      proof

        reconsider N = M as ManySortedSubset of M by PBOOLE:def 18;

        reconsider N1 = N as OrderSortedSubset of M by Def1;

        take N1;

        thus thesis;

      end;

    end

    begin

    definition

      let S be OrderSortedSign, U0 be OSAlgebra of S;

      :: OSALG_2:def2

      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 PBOOLE:def 18;

        take B;

        thus thesis by OSALG_1: 17;

      end;

    end

    registration

      let S be OrderSortedSign;

      cluster monotone strict non-empty for OSAlgebra of S;

      existence

      proof

        set z1 = the Element of { {} };

        take ( TrivialOSA (S, { {} },z1));

        thus thesis;

      end;

    end

    registration

      let S be OrderSortedSign, U0 be non-empty OSAlgebra of S;

      cluster non-empty for OSSubset of U0;

      existence

      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;

        thus thesis;

      end;

    end

    theorem :: OSALG_2:3



     Th3: for S0 be 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 5;

      s1 is with_const_op by MSUALG_2:def 2;

      then

      consider o be Element of the carrier' of S0 such that

       A1: (the Arity of S0 . o) = {} & (the ResultSort of S0 . o) = s1;



       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 thesis by A2;

    end;

    registration

      cluster all-with_const_op strict for OrderSortedSign;

      existence

      proof

        set S0 = the non void all-with_const_op strict non empty ManySortedSign;

        take ( OSSign S0);

        thus thesis by Th3;

      end;

    end

    begin

    theorem :: OSALG_2:4



     Th4: for S be OrderSortedSign, U0 be 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;

      the Sorts of U0 is OrderSortedSet of S by OSALG_1: 17;

      hence thesis by OSALG_1: 17;

    end;

    registration

      let S be OrderSortedSign, U0 be OSAlgebra of S;

      cluster order-sorted for MSSubAlgebra of U0;

      existence

      proof

        reconsider U1 = MSAlgebra (# the Sorts of U0, the Charact of U0 #) as strict MSSubAlgebra of U0 by MSUALG_2: 37;

        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

    registration

      let S be OrderSortedSign, U0 be OSAlgebra of S;

      cluster strict for 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: 37;

        take U1;

        thus thesis;

      end;

    end

    registration

      let S be OrderSortedSign, U0 be non-empty OSAlgebra of S;

      cluster non-empty strict for 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: 37, OSALG_1: 17;

        take U1;

        thus thesis;

      end;

    end

    theorem :: OSALG_2:5



     Th5: for S be OrderSortedSign holds for U0 be OSAlgebra of S holds for U1 be 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 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;

        let B be OSSubset of U0;

        assume B = the Sorts of U1;

        hence B is opers_closed & the Charact of U1 = ( Opers (U0,B)) by A1, MSUALG_2:def 9;

      end;

      assume

       A2: the Sorts of U1 is OSSubset of U0;

      assume

       A3: for B be OSSubset of U0 st B = the Sorts of U1 holds B is opers_closed & the Charact of U1 = ( Opers (U0,B));



       A4: U1 is MSSubAlgebra of U0

      proof

        thus the Sorts of U1 is MSSubset of U0 by A2;

        let B be MSSubset of U0 such that

         A5: B = the Sorts of U1;

        reconsider B1 = B as OSSubset of U0 by A2, A5;

        B1 is opers_closed by A3, A5;

        hence thesis by A3, A5;

      end;

      the Sorts of U1 is OrderSortedSet of S by A2, Def2;

      hence thesis by A4, 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;

      :: OSALG_2:def3

      func OSConstants (OU0,s) -> Subset of (the Sorts of OU0 . s) equals ( union { ( Constants (OU0,s2)) : s2 <= s });

      coherence

      proof

        set Cs = { ( Constants (OU0,s2)) : s2 <= s };

        for X be set st X in Cs holds X c= (the Sorts of OU0 . s)

        proof

          let X be set;

          assume X in Cs;

          then

          consider s2 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 thesis by A1;

        end;

        hence thesis by ZFMISC_1: 76;

      end;

    end

    theorem :: OSALG_2:6



     Th6: ( Constants (OU0,s)) c= ( OSConstants (OU0,s))

    proof

      ( Constants (OU0,s)) in { ( Constants (OU0,s2)) : s2 <= s };

      hence thesis by ZFMISC_1: 74;

    end;

    definition

      let S1;

      let M be ManySortedSet of the carrier of S1;

      :: OSALG_2:def4

      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 FUNCT_1:sch 4;

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

          assume

           A2: r1 <= r2;

          let x be object;

          assume x in (f1 . r1);

          then x in ( union { (M . s2) : s2 <= r1 }) by A1;

          then

          consider y be set such that

           A3: x in y & y in { (M . s2) : s2 <= r1 } by TARSKI:def 4;

          consider s3 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) : s2 <= r2 } by A4;

          then x in ( union { (M . s2) : s2 <= r2 }) by A3, TARSKI:def 4;

          hence thesis 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 be SortSymbol of S1 holds (W1 . s) = ( union { (M . s1) : s1 <= s });

        assume

         A7: for s be SortSymbol of S1 holds (W2 . s) = ( union { (M . s1) : s1 <= s });

        for s be object st s in the carrier of S1 holds (W1 . s) = (W2 . s)

        proof

          let s be object;

          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;

      end;

    end

    theorem :: OSALG_2:7



     Th7: for M be ManySortedSet of the carrier of S1 holds M c= ( OSCl M)

    proof

      let M be ManySortedSet of the carrier of S1;

      let i be object;

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

      hence thesis by Def4;

    end;

    theorem :: OSALG_2:8



     Th8: for M be ManySortedSet of the carrier of S1, A be 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 be object such that

       A2: i in the carrier of S1 and

       A3: not (( OSCl M) . i) c= (A . i);

      reconsider s = i as SortSymbol of S1 by A2;

      consider x be object such that

       A4: x in (( OSCl M) . i) and

       A5: not x in (A . i) by A3;

      (( OSCl M) . s) = ( union { (M . s2) : s2 <= s }) by Def4;

      then

      consider X1 be set such that

       A6: x in X1 and

       A7: X1 in { (M . s2) : s2 <= s } by A4, TARSKI:def 4;

      consider s1 be SortSymbol of S1 such that

       A8: X1 = (M . s1) and

       A9: s1 <= s by A7;

      (M . s1) c= (A . s1) by A1;

      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;

    end;

    theorem :: OSALG_2:9

    for S be OrderSortedSign, X be 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 Th7, Th8;

      hence thesis by PBOOLE: 146;

    end;

    definition

      let S1, OU0;

      :: OSALG_2:def5

      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 FUNCT_1:sch 4;

        reconsider 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 object;

          assume s in the carrier of S1;

          then

          reconsider s1 = s as SortSymbol of S1;

          (f . s1) = ( OSConstants (OU0,s1)) by A1;

          hence thesis;

        end;

        then

        reconsider f as MSSubset of OU0 by PBOOLE:def 18;

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

          assume x in (f1 . r1);

          then x in ( union { ( Constants (OU0,s2)) : s2 <= r1 }) by A1;

          then

          consider y be set such that

           A3: x in y & y in { ( Constants (OU0,s2)) : s2 <= r1 } by TARSKI:def 4;

          consider s3 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)) : s2 <= r2 } by A4;

          then x in ( union { ( Constants (OU0,s2)) : s2 <= r2 }) by A3, TARSKI:def 4;

          hence thesis by A1;

        end;

        hence f is OSSubset of OU0 by Def2;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let W1,W2 be OSSubset of OU0;

        assume that

         A6: for s be SortSymbol of S1 holds (W1 . s) = ( OSConstants (OU0,s)) and

         A7: for s be SortSymbol of S1 holds (W2 . s) = ( OSConstants (OU0,s));

        for s be object st s in the carrier of S1 holds (W1 . s) = (W2 . s)

        proof

          let s be object;

          assume s in the carrier of S1;

          then

          reconsider t = s as SortSymbol of S1;

          (W1 . t) = ( OSConstants (OU0,t)) by A6;

          hence thesis by A7;

        end;

        hence thesis;

      end;

    end

    theorem :: OSALG_2:10



     Th10: ( Constants OU0) c= ( OSConstants OU0)

    proof

      let i be object;

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

      hence thesis by Th6;

    end;

    theorem :: OSALG_2:11



     Th11: for A be 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;

      assume not ( OSConstants OU0) c= A;

      then

      consider i be object such that

       A2: i in the carrier of S1 and

       A3: not (( OSConstants OU0) . i) c= (A . i);

      reconsider s = i as SortSymbol of S1 by A2;

      consider x be object such that

       A4: x in (( OSConstants OU0) . i) and

       A5: not x in (A . i) by A3;

      (( OSConstants OU0) . s) = ( OSConstants (OU0,s)) by Def5

      .= ( union { ( Constants (OU0,s2)) : s2 <= s });

      then

      consider X1 be set such that

       A6: x in X1 and

       A7: X1 in { ( Constants (OU0,s2)) : s2 <= s } by A4, TARSKI:def 4;

      consider s1 be 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;

      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;

    end;

    theorem :: OSALG_2:12

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

    proof

      let A be OSSubset of OU0;

       A1:

      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 be object holds (x in c1 iff x in c2)

        proof

          let x be object;

          hereby

            assume x in c1;

            then

            consider 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 c2 by A3;

          end;

          assume x in c2;

          then

          consider s1 such that

           A4: x = ( Constants (OU0,s1)) and

           A5: s1 <= s;

          x = (( Constants OU0) . s1) by A4, MSUALG_2:def 4;

          hence thesis by A5;

        end;

        then

         A6: c1 = c2 by TARSKI: 2;

        (( OSConstants OU0) . s) = ( OSConstants (OU0,s)) by Def5

        .= (( OSCl ( Constants OU0)) . s) by A6, Def4;

        hence (( OSConstants OU0) . i) = (( OSCl ( Constants OU0)) . i);

      end;

      then for i be object st i in the carrier of S1 holds (( OSCl ( Constants OU0)) . i) c= (( OSConstants OU0) . i);

      then

       A7: ( OSCl ( Constants OU0)) c= ( OSConstants OU0);

      for i be object 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));

      hence thesis by A7, PBOOLE: 146;

    end;

    theorem :: OSALG_2:13



     Th13: for OU1 be OSSubAlgebra of OU0 holds ( OSConstants OU0) is OSSubset of OU1

    proof

      let OU1 be OSSubAlgebra of OU0;

      ( OSConstants OU0) c= the Sorts of OU1

      proof

        let i be object;

        assume i in the carrier of S1;

        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 st s2 <= s3 holds (( Constants OU0) . s2) c= (the Sorts of OU1 . s3)

        proof

          let s2, s3;

          assume s2 <= 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;

          hence thesis by A3;

        end;



         A4: for X be 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

           A5: X = ( Constants (OU0,s4)) & s4 <= s;

          ( Constants (OU0,s4)) = (( Constants OU0) . s4) by MSUALG_2:def 4;

          hence thesis by A2, A5;

        end;

        (( OSConstants OU0) . i) = ( OSConstants (OU0,s)) by Def5

        .= ( union { ( Constants (OU0,s1)) : s1 <= s });

        hence thesis by A4, ZFMISC_1: 76;

      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 thesis by A6, Def2;

    end;

    theorem :: OSALG_2:14

    for S be all-with_const_op OrderSortedSign, OU0 be non-empty OSAlgebra of S, OU1 be 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 Th10;

      hence thesis by Th13, PBOOLE: 131;

    end;

    begin

    theorem :: OSALG_2:15



     Th15: for I be set holds for M be ManySortedSet of I holds for x be 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 PARTFUN1:def 2;

      hereby

        assume x is ManySortedSubset of M;

        then

        reconsider x1 = x as ManySortedSubset of M;



         A2: for i be object st i in ( dom ( bool M)) holds (x1 . i) in (( bool M) . i)

        proof

          let i be object such that

           A3: i in ( dom ( bool M));

          x1 c= M by PBOOLE:def 18;

          then (x1 . i) c= (M . i) by A1, A3;

          then (x1 . i) in ( bool (M . i));

          hence thesis by A1, A3, MBOOLEAN:def 1;

        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;

      end;

      assume x in ( product ( bool M));

      then

      consider x1 be Function such that

       A4: x = x1 and

       A5: ( dom x1) = ( dom ( bool M)) and

       A6: for i be object 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 object such that

         A7: i in I;

        (x2 . i) in (( bool M) . i) by A1, A6, A7;

        then (x2 . i) in ( bool (M . i)) by A7, MBOOLEAN:def 1;

        hence thesis;

      end;

      hence thesis by A4, PBOOLE:def 18;

    end;

    definition

      let R be non empty Poset, M be OrderSortedSet of R;

      :: OSALG_2:def6

      func OSbool (M) -> set means for x be set holds x in it iff x is OrderSortedSubset of M;

      existence

      proof

        defpred P[ set] means $1 is OrderSortedSubset of M;

        set f = ( product ( bool M));

        consider X be set such that

         A1: for y be set holds y in X iff y in f & P[y] from XFAMILY:sch 1;

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

        hence thesis by A1, A2;

      end;

      uniqueness

      proof

        defpred P[ set] means $1 is OrderSortedSubset of M;

        thus for X1,X2 be set st (for x be set holds x in X1 iff P[x]) & (for x be set holds x in X2 iff P[x]) holds X1 = X2 from XFAMILY:sch 3;

      end;

    end

    definition

      let S be OrderSortedSign, U0 be OSAlgebra of S, A be OSSubset of U0;

      :: OSALG_2:def7

      func OSSubSort (A) -> set equals { x where x be Element of ( SubSort A) : x is OrderSortedSet of S };

      correctness ;

    end

    theorem :: OSALG_2:16



     Th16: for A be OSSubset of OU0 holds ( OSSubSort A) c= ( SubSort A)

    proof

      let A be OSSubset of OU0;

      let x be object;

      assume x in ( OSSubSort A);

      then ex y be Element of ( SubSort A) st x = y & y is OrderSortedSet of S1;

      hence thesis;

    end;

    theorem :: OSALG_2:17



     Th17: for A be 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: 38;

      the Sorts of OU0 is OrderSortedSet of S1 by OSALG_1: 17;

      then X in { x where x be Element of ( SubSort A) : x is OrderSortedSet of S1 };

      hence thesis;

    end;

    registration

      let S1, OU0;

      let A be OSSubset of OU0;

      cluster ( OSSubSort A) -> non empty;

      coherence by Th17;

    end

    definition

      let S1, OU0;

      :: OSALG_2:def8

      func OSSubSort (OU0) -> set equals { x where x be Element of ( SubSort OU0) : x is OrderSortedSet of S1 };

      correctness ;

    end

    theorem :: OSALG_2:18



     Th18: for A be OSSubset of OU0 holds ( OSSubSort A) c= ( OSSubSort OU0)

    proof

      let A be OSSubset of OU0;

      let x be object;

      assume x in ( OSSubSort A);

      then

      consider x1 be 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 be Element of ( SubSort OU0) : y is OrderSortedSet of S1 } by A2;

      hence thesis by A1;

    end;

    registration

      let S1, OU0;

      cluster ( OSSubSort OU0) -> non empty;

      coherence

      proof

        set A = the OSSubset of OU0;

        ( OSSubSort A) c= ( OSSubSort OU0) by Th18;

        hence thesis;

      end;

    end

    definition

      let S1, OU0;

      let e be Element of ( OSSubSort OU0);

      :: OSALG_2:def9

      func @ e -> OSSubset of OU0 equals e;

      coherence

      proof

        e in { x where x be Element of ( SubSort OU0) : x is OrderSortedSet of S1 };

        then

        consider e1 be 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 thesis;

      end;

    end

    theorem :: OSALG_2:19



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

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

      proof

        assume B in ( OSSubSort A);

        then

         A1: ex B1 be Element of ( SubSort A) st B1 = B & B1 is OrderSortedSet of S1;

        then ( Constants OU0) c= B by MSUALG_2: 13;

        hence thesis by A1, Th11, MSUALG_2: 13;

      end;

      assume that

       A2: B is opers_closed and

       A3: ( OSConstants OU0) c= B and

       A4: A c= B;

      ( 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 thesis by A5;

    end;

    theorem :: OSALG_2:20



     Th20: 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 in ( SubSort OU0) iff B is opers_closed by MSUALG_2: 14;

      thus B in ( OSSubSort OU0) implies B is opers_closed

      proof

        assume B in ( OSSubSort OU0);

        then ex B1 be Element of ( SubSort OU0) st B1 = B & B1 is OrderSortedSet of S1;

        hence thesis by MSUALG_2: 14;

      end;

      assume

       A2: B is opers_closed;

      B is OrderSortedSet of S1 by Def2;

      hence thesis by A1, A2;

    end;

    definition

      let S1, OU0;

      let A be OSSubset of OU0, s be Element of S1;

      :: OSALG_2:def10

      func OSSubSort (A,s) -> set means

      : Def10: for x be object holds x in it iff ex B be OSSubset of OU0 st B in ( OSSubSort A) & x = (B . s);

      existence

      proof

        defpred P[ object] means ex B be OSSubset of OU0 st B in ( OSSubSort A) & $1 = (B . s);

        set C = ( bool ( Union the Sorts of OU0));

        consider X be set such that

         A1: for x be object holds x in X iff x in C & P[x] from XBOOLE_0:sch 1;

        take X;



         A2: C = ( bool ( union ( rng the Sorts of OU0))) by CARD_3:def 4;

        for x be set holds x in X iff ex B be 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;

          thus x in X implies ex B be OSSubset of OU0 st B in ( OSSubSort A) & x = (B . s) by A1;

          given B be OSSubset of OU0 such that

           A4: B in ( OSSubSort A) and

           A5: x = (B . s);

          B c= the Sorts of OU0 by PBOOLE:def 18;

          then (B . s) c= (the Sorts of OU0 . s);

          then x c= ( union ( rng the Sorts of OU0)) by A5, A3;

          hence thesis by A2, A1, A4, A5;

        end;

        hence thesis;

      end;

      uniqueness

      proof

        defpred P[ object] means ex B be OSSubset of OU0 st B in ( OSSubSort A) & $1 = (B . s);

        thus for X1,X2 be set st (for x be object holds x in X1 iff P[x]) & (for x be object holds x in X2 iff P[x]) holds X1 = X2 from XBOOLE_0:sch 3;

      end;

    end

    theorem :: OSALG_2:21



     Th21: for A be OSSubset of OU0, s1,s2 be 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 be set st Y in ( OSSubSort (A,s2)) holds ex X be set st X in ( OSSubSort (A,s1)) & X c= Y

      proof

        let x be set;

        assume x in ( OSSubSort (A,s2));

        then

        consider B be OSSubset of OU0 such that

         A2: B in ( OSSubSort A) & x = (B . s2) by Def10;

        take (B . s1);

        B is OrderSortedSet of S1 by Def2;

        hence thesis by A1, A2, Def10, OSALG_1:def 16;

      end;

      hence thesis by SETFAM_1:def 3;

    end;

    theorem :: OSALG_2:22



     Th22: for A be OSSubset of OU0, s be 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 object;

      assume x in ( OSSubSort (A,s));

      then

       A1: ex B be OSSubset of OU0 st B in ( OSSubSort A) & x = (B . s) by Def10;

      ( OSSubSort A) c= ( SubSort A) by Th16;

      hence thesis by A1, MSUALG_2:def 13;

    end;

    theorem :: OSALG_2:23



     Th23: for A be OSSubset of OU0, s be 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;

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

    end;

    registration

      let S1, OU0;

      let A be OSSubset of OU0, s be SortSymbol of S1;

      cluster ( OSSubSort (A,s)) -> non empty;

      coherence by Th23;

    end

    definition

      let S1, OU0;

      let A be OSSubset of OU0;

      :: OSALG_2:def11

      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 FUNCT_1:sch 4;

        reconsider 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 object;

          assume x in the carrier of S1;

          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 thesis by A2, SETFAM_1: 3;

        end;

        then

        reconsider f as MSSubset of OU0 by PBOOLE:def 18;

        take f;

        reconsider f1 = f as ManySortedSet of S1;

        for s1,s2 be Element of S1 st s1 <= s2 holds (f1 . s1) c= (f1 . s2)

        proof

          let s1,s2 be Element of S1;

          assume s1 <= 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 thesis by A1, A4;

        end;

        then f is OrderSortedSet of S1 by OSALG_1:def 16;

        hence thesis by A1, Def2;

      end;

      uniqueness

      proof

        let W1,W2 be OSSubset of OU0;

        assume that

         A5: for s be SortSymbol of S1 holds (W1 . s) = ( meet ( OSSubSort (A,s))) and

         A6: for s be SortSymbol of S1 holds (W2 . s) = ( meet ( OSSubSort (A,s)));

        for s be object st s in the carrier of S1 holds (W1 . s) = (W2 . s)

        proof

          let s be object;

          assume s in the carrier of S1;

          then

          reconsider s as SortSymbol of S1;

          (W1 . s) = ( meet ( OSSubSort (A,s))) by A5;

          hence thesis by A6;

        end;

        hence thesis;

      end;

    end

    registration

      let S1, OU0;

      cluster opers_closed for OSSubset of OU0;

      existence

      proof

        set x = the Element of ( OSSubSort OU0);

        x in { y where y be Element of ( SubSort OU0) : y is OrderSortedSet of S1 };

        then

        consider x1 be Element of ( SubSort OU0) such that x = 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;

        thus thesis by MSUALG_2:def 11;

      end;

    end

    theorem :: OSALG_2:24



     Th24: for A be OSSubset of OU0 holds (( OSConstants OU0) (\/) A) c= ( OSMSubSort A)

    proof

      let A be OSSubset of OU0;

      let i be object;

      assume i in the carrier of S1;

      then

      reconsider s = i as SortSymbol of S1;



       A1: 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) 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 thesis by A3;

      end;

      (( OSMSubSort A) . s) = ( meet ( OSSubSort (A,s))) by Def11;

      hence thesis by A1, SETFAM_1: 5;

    end;

    theorem :: OSALG_2:25

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

        assume i in the carrier of S1;

        then

        reconsider s = i as SortSymbol of S1;

        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) 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 thesis by A3;

        end;

        then

         A4: ((( OSConstants OU0) (\/) A) . s) c= ( meet ( OSSubSort (A,s))) by SETFAM_1: 5;

        ex x be object st x in ((( OSConstants OU0) (\/) A) . s) by A1, XBOOLE_0:def 1;

        hence (( OSMSubSort A) . i) is non empty by A4, Def11;

      end;

      hence thesis;

    end;

    theorem :: OSALG_2:26



     Th26: for o be OperSymbol of S1 holds for A be OSSubset of OU0 holds 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 object;

        assume i in the carrier of S1;

        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 thesis by SETFAM_1: 3;

      end;

      hence thesis by MSUALG_2: 2;

    end;

    theorem :: OSALG_2:27



     Th27: for o be OperSymbol of S1 holds for A be OSSubset of OU0 holds 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 B is opers_closed by Th19;

      then B is_closed_on o;

      then

       A2: ( rng (d | b)) c= ((B * the ResultSort of S1) . o);

      (b /\ m) = m by A1, Th26, XBOOLE_1: 28;

      then (d | m) = ((d | b) | m) by RELAT_1: 71;

      then ( rng (d | m)) c= ( rng (d | b)) by RELAT_1: 70;

      hence thesis by A2;

    end;

    theorem :: OSALG_2:28



     Th28: for o be OperSymbol of S1 holds 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 object;

      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) & ( 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) . r) by FUNCT_1: 13

      .= ( meet ( OSSubSort (A,r))) by Def11;

      then

      consider X be set such that

       A4: X in ( OSSubSort (A,r)) and

       A5: not x in X by A2, SETFAM_1:def 1;

      consider B be OSSubset of OU0 such that

       A6: B in ( OSSubSort A) and

       A7: (B . r) = 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;

    end;

    theorem :: OSALG_2:29



     Th29: 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 carrier' 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 Th28;

        hence thesis;

      end;

      A c= (( OSConstants OU0) (\/) A) & (( OSConstants OU0) (\/) A) c= ( OSMSubSort A) by Th24, PBOOLE: 14;

      hence thesis by PBOOLE: 13;

    end;

    registration

      let S1, OU0;

      let A be OSSubset of OU0;

      cluster ( OSMSubSort A) -> opers_closed;

      coherence by Th29;

    end

    begin

    registration

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

        (OU0 | A) = M & A is OrderSortedSet of S1 by Def2, MSUALG_2:def 15;

        hence thesis by OSALG_1: 17;

      end;

    end

    registration

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

        hence thesis by OSALG_1: 17;

      end;

    end

    definition

      let S1, OU0;

      let A be OSSubset of OU0;

      :: OSALG_2:def12

      func GenOSAlg (A) -> strict OSSubAlgebra of OU0 means

      : Def12: 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

        set a = ( OSMSubSort A);

        reconsider u1 = (OU0 | a) as strict OSSubAlgebra of OU0;

        take u1;



         A1: u1 = MSAlgebra (# a, ( Opers (OU0,a)) qua ManySortedFunction of ((a # ) * the Arity of S1), (a * the ResultSort of S1) #) by MSUALG_2:def 15;



         A2: A is OrderSortedSet of S1 by Def2;

        A c= a by Th29;

        then A is MSSubset of u1 by A1, PBOOLE:def 18;

        hence A is OSSubset of u1 by A2, Def2;

        let U2 be OSSubAlgebra of OU0;

        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;

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

          assume i in the carrier of S1;

          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 thesis by SETFAM_1: 3;

        end;

        hence thesis by MSUALG_2: 8;

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

      end;

    end

    theorem :: OSALG_2:30



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

      set a = ( OSMSubSort A);

      reconsider u1 = (OU0 | a) as strict OSSubAlgebra of OU0;



       A1: u1 = MSAlgebra (# a, ( Opers (OU0,a)) qua ManySortedFunction of ((a # ) * the Arity of S1), (a * the ResultSort of S1) #) by MSUALG_2:def 15;



       A2: A c= a by Th29;



       A3: A is OrderSortedSet of S1 by Def2;



       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, A1, PBOOLE:def 18;

        hence A is OSSubset of u1 by A3, Def2;

        let U2 be OSSubAlgebra of OU0;

        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;

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

          assume i in the carrier of S1;

          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 thesis by SETFAM_1: 3;

        end;

        hence thesis by MSUALG_2: 8;

      end;

      hence ( GenOSAlg A) = (OU0 | a) by Def12;

      thus thesis by A1, A4, Def12;

    end;

    theorem :: OSALG_2:31



     Th31: for S be non void non empty ManySortedSign holds for U0 be MSAlgebra over S holds 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);

      reconsider u1 = (U0 | a) as strict MSSubAlgebra of U0;



       A1: u1 = MSAlgebra (# a, ( Opers (U0,a)) qua ManySortedFunction of ((a # ) * the Arity of S), (a * the ResultSort of S) #) by MSUALG_2: 20, MSUALG_2:def 15;



       A2: A c= a by MSUALG_2: 20;



       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 A2, A1, PBOOLE:def 18;

        let U2 be MSSubAlgebra of U0;

        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;

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

          assume i in the carrier of S;

          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 thesis by SETFAM_1: 3;

        end;

        hence thesis by MSUALG_2: 8;

      end;

      hence ( GenMSAlg A) = (U0 | a) by MSUALG_2:def 17;

      thus thesis by A1, A3, MSUALG_2:def 17;

    end;

    theorem :: OSALG_2:32



     Th32: for A be 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);

      let i be object;

      assume i in the carrier of S1;

      then

      reconsider s = i as SortSymbol of S1;

      the Sorts of GM = ( MSSubSort A) by Th31;

      then

       A1: (the Sorts of GM . s) = ( meet ( SubSort (A,s))) by MSUALG_2:def 14;

      the Sorts of GO = ( OSMSubSort A) by Th30;

      then (the Sorts of GO . s) = ( meet ( OSSubSort (A,s))) by Def11;

      hence thesis by A1, Th22, SETFAM_1: 6;

    end;

    theorem :: OSALG_2:33

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

    theorem :: OSALG_2:34



     Th34: for OU0 be strict OSAlgebra of S1 holds for B be 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: 21;

      ( GenMSAlg B) is strict MSSubAlgebra of ( GenOSAlg B) by Th32, MSUALG_2: 8;

      hence thesis by A1, MSUALG_2: 7;

    end;

    theorem :: OSALG_2:35



     Th35: for OU1 be strict OSSubAlgebra of OU0, B be 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;

      set W = ( GenOSAlg B);

      assume

       A1: B = the Sorts of OU1;

      then

       A2: B is MSSubset of OU1 by PBOOLE:def 18;

      B is OSSubset of W by Def12;

      then the Sorts of OU1 c= the Sorts of W by A1, PBOOLE:def 18;

      then

       A3: OU1 is strict MSSubAlgebra of W by MSUALG_2: 8;

      B is OrderSortedSet of S1 by Def2;

      then B is OSSubset of OU1 by A2, Def2;

      then W is strict OSSubAlgebra of OU1 by Def12;

      hence thesis by A3, MSUALG_2: 7;

    end;

    theorem :: OSALG_2:36



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

      C is OSSubset of U1 by Th13;

      then G is strict OSSubAlgebra of U1 by Def12;

      then the Sorts of G is MSSubset of U1 by MSUALG_2:def 9;

      then the Sorts of (G /\ U1) = (the Sorts of G (/\) the Sorts of U1) & the Sorts of G c= the Sorts of U1 by MSUALG_2:def 16, PBOOLE:def 18;

      then the Sorts of (G /\ U1) = the Sorts of G by PBOOLE: 23;

      hence thesis by MSUALG_2: 9;

    end;

    definition

      let S1;

      let U0 be non-empty OSAlgebra of S1, U1,U2 be OSSubAlgebra of U0;

      :: OSALG_2:def13

      func U1 "\/"_os U2 -> strict OSSubAlgebra of U0 means

      : Def13: 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 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 B c= the Sorts of U0 by A1, PBOOLE: 16;

        then

        reconsider B 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);

        thus thesis;

      end;

      uniqueness

      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 B c= the Sorts of U0 by A2, PBOOLE: 16;

        then

        reconsider B as MSSubset of U0 by PBOOLE:def 18;

        let W1,W2 be strict OSSubAlgebra of U0;

        assume that

         A3: for A be OSSubset of U0 st A = (the Sorts of U1 (\/) the Sorts of U2) holds W1 = ( GenOSAlg A) and

         A4: for A be OSSubset of U0 st A = (the Sorts of U1 (\/) the Sorts of U2) holds W2 = ( GenOSAlg A);

        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 thesis by A4;

      end;

    end

    theorem :: OSALG_2:37



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

      assume

       A1: B = (A (\/) the Sorts of U1);

      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 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 thesis by A4, A13, MSUALG_2: 7;

    end;

    theorem :: OSALG_2:38



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



       A1: the Sorts of U1 is MSSubset of U0 by MSUALG_2:def 9;

      assume B = the Sorts of U0;

      then the Sorts of U1 c= B by A1, PBOOLE:def 18;

      then (B (\/) the Sorts of U1) = B by PBOOLE: 22;

      hence thesis by Th37;

    end;

    theorem :: OSALG_2:39



     Th39: for U0 be 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 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 thesis by Def13;

    end;

    theorem :: OSALG_2:40



     Th40: 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 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 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 thesis by A1, MSUALG_2:def 9;

    end;

    theorem :: OSALG_2:41



     Th41: 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 9;



       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 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 thesis by A2, Th35;

    end;

    begin

    definition

      let S1, OU0;

      :: OSALG_2:def14

      func OSSub (OU0) -> set means

      : Def14: for x be object holds x in it iff x is strict OSSubAlgebra of OU0;

      existence

      proof

        set X = the set of all ( GenOSAlg ( @ A)) where A be Element of ( OSSubSort OU0);

        take X;

        let x be object;

        thus x in X implies x is strict OSSubAlgebra of OU0

        proof

          assume x in X;

          then ex A be Element of ( OSSubSort OU0) st x = ( GenOSAlg ( @ A));

          hence thesis;

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

        a = ( GenOSAlg ( @ h)) by Th35;

        hence thesis;

      end;

      uniqueness

      proof

        defpred P[ object] means $1 is strict OSSubAlgebra of OU0;

        thus for X1,X2 be set st (for x be object holds x in X1 iff P[x]) & (for x be object holds x in X2 iff P[x]) holds X1 = X2 from XBOOLE_0:sch 3;

      end;

    end

    theorem :: OSALG_2:42



     Th42: ( OSSub OU0) c= ( MSSub OU0)

    proof

      let x be object;

      assume x in ( OSSub OU0);

      then x is strict MSSubAlgebra of OU0 by Def14;

      hence thesis by MSUALG_2:def 19;

    end;

    registration

      let S be OrderSortedSign, U0 be OSAlgebra of S;

      cluster ( OSSub U0) -> non empty;

      coherence

      proof

        set x = the strict OSSubAlgebra of U0;

        x in ( OSSub U0) by Def14;

        hence thesis;

      end;

    end

    definition

      let S1, OU0;

      :: original: OSSub

      redefine

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

      coherence by Th42;

    end

    definition

      let S1;

      let U0 be non-empty OSAlgebra of S1;

      :: OSALG_2:def15

      func OSAlg_join (U0) -> BinOp of ( OSSub U0) means

      : Def15: 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), set] means for U1,U2 be strict OSSubAlgebra of U0 st $1 = U1 & $2 = U2 holds $3 = (U1 "\/"_os U2);



         A1: for x,y be Element of ( OSSub U0) holds ex z be 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 Def14;

          reconsider z = (U1 "\/"_os U2) as Element of ( OSSub U0) by Def14;

          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 BINOP_1:sch 3( A1);

        take o;

        thus thesis by A2;

      end;

      uniqueness

      proof

        let o1,o2 be BinOp of ( OSSub U0);

        assume that

         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) and

         A4: 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) holds 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 Def14;

          (o1 . (x,y)) = (U1 "\/"_os U2) by A3;

          hence thesis by A4;

        end;

        hence thesis by BINOP_1: 2;

      end;

    end

    definition

      let S1;

      let U0 be non-empty OSAlgebra of S1;

      :: OSALG_2:def16

      func OSAlg_meet (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 /\ U2);

      existence

      proof

        defpred P[ Element of ( OSSub U0), Element of ( OSSub U0), set] means for U1,U2 be strict OSSubAlgebra of U0 st $1 = U1 & $2 = U2 holds $3 = (U1 /\ U2);



         A1: for x,y be Element of ( OSSub U0) holds ex z be 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 Def14;

          reconsider z = (U1 /\ U2) as Element of ( OSSub U0) by Def14;

          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 BINOP_1:sch 3( A1);

        take o;

        thus thesis by A2;

      end;

      uniqueness

      proof

        let o1,o2 be BinOp of ( OSSub U0);

        assume that

         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) and

         A4: 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) holds 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 Def14;

          (o1 . (x,y)) = (U1 /\ U2) by A3;

          hence thesis by A4;

        end;

        hence thesis by BINOP_1: 2;

      end;

    end

    theorem :: OSALG_2:43



     Th43: for U0 be non-empty OSAlgebra of S1 holds for x,y be 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 Def14;

      then

      consider U1,U2 be 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 thesis;

    end;

    reserve U0 for non-empty OSAlgebra of S1;

    theorem :: OSALG_2:44



     Th44: ( 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 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 B c= the Sorts of U0 by A1, PBOOLE: 16;

        then

         A2: B 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 B is OrderSortedSet of S1 by Th2;

        then

        reconsider B as OSSubset of U0 by A2, Def2;



         A3: (U1 "\/"_os U2) = ( GenOSAlg B) by Def13;

        (o . (x,y)) = (U1 "\/"_os U2) & (o . (y,x)) = (U2 "\/"_os U1) by Def15;

        hence thesis by A3, Def13;

      end;

      hence thesis by BINOP_1:def 2;

    end;

    theorem :: OSALG_2:45



     Th45: ( 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 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: B 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;

        (o . (y,z)) = (U2 "\/"_os U3) by Def15;

        then

         A8: (o . (x,(o . (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: (o . (x,y)) = (U1 "\/"_os U2) by Def15;

        B c= the Sorts of U0 by A7, A3, PBOOLE: 16;

        then B is MSSubset of U0 by PBOOLE:def 18;

        then

        reconsider B 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 thesis by A9, A8, A11, Def15;

      end;

      hence thesis by BINOP_1:def 3;

    end;

    theorem :: OSALG_2:46



     Th46: ( OSAlg_meet U0) is commutative

    proof

      set o = ( OSAlg_meet U0);

      set m = ( MSAlg_meet U0);



       A1: m is commutative by MSUALG_2: 31;

      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 Th43

        .= (m . (y,x)) by A1, BINOP_1:def 2

        .= (o . (y,x)) by Th43;

        hence thesis;

      end;

      hence thesis by BINOP_1:def 2;

    end;

    theorem :: OSALG_2:47



     Th47: ( OSAlg_meet U0) is associative

    proof

      set o = ( OSAlg_meet U0);

      set m = ( MSAlg_meet U0);



       A1: m is associative by MSUALG_2: 32;

      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 . (x,y)) = (m . (x,y)) by Th43;

        (o . (y,z)) = (m . (y,z)) by Th43;



        then (o . (x,(o . (y,z)))) = (m . (x,(m . (y,z)))) by Th43

        .= (m . ((m . (x,y)),z)) by A1, BINOP_1:def 3

        .= (o . ((o . (x,y)),z)) by A2, Th43;

        hence thesis;

      end;

      hence thesis by BINOP_1:def 3;

    end;

    definition

      let S1;

      let U0 be non-empty OSAlgebra of S1;

      :: OSALG_2:def17

      func OSSubAlLattice (U0) -> strict Lattice equals 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,c be Element of L holds (a "\/" (b "\/" c)) = ((a "\/" b) "\/" c) by Th45, BINOP_1:def 3;



         A2: for a,b be Element of L holds (a "/\" b) = (b "/\" a) by Th46, BINOP_1:def 2;



         A3: for a,b be 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);

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

          end;

          hence thesis;

        end;



         A4: for a,b be 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);

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

          end;

          hence thesis;

        end;



         A5: for a,b,c be Element of L holds (a "/\" (b "/\" c)) = ((a "/\" b) "/\" c) by Th47, BINOP_1:def 3;

        for a,b be Element of L holds (a "\/" b) = (b "\/" a) by Th44, BINOP_1:def 2;

        then L is strict join-commutative join-associative meet-absorbing meet-commutative meet-associative join-absorbing by A1, A4, A2, A5, A3;

        hence thesis;

      end;

    end

    theorem :: OSALG_2:48



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

      thus L is lower-bounded

      proof

        set C = ( OSConstants U0);

        reconsider G = ( GenOSAlg C) as Element of ( OSSub U0) by Def14;

        reconsider G1 = G as Element of L;

        take G1;

        let a be Element of L;

        reconsider a1 = a as Element of ( OSSub U0);

        reconsider a2 = a1 as strict OSSubAlgebra of U0 by Def14;



        thus (G1 "/\" a) = (( GenOSAlg C) /\ a2) by Def16

        .= G1 by Th36;

        hence thesis;

      end;

      thus L is upper-bounded

      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 as OSSubset of U0 by Def2;

        reconsider G = ( GenOSAlg B) as Element of ( OSSub U0) by Def14;

        reconsider G1 = G as Element of L;

        take G1;

        let a be Element of L;

        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;

        hence thesis;

      end;

    end;

    registration

      let S1;

      let U0 be non-empty OSAlgebra of S1;

      cluster ( OSSubAlLattice U0) -> bounded;

      coherence by Th48;

    end

    theorem :: OSALG_2:49

    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 C = ( OSConstants U0);

      reconsider G = ( GenOSAlg C) as Element of ( OSSub U0) by Def14;

      set L = ( OSSubAlLattice U0);

      reconsider G1 = G as Element of L;

      now

        let a be Element of L;

        reconsider a1 = a as Element of ( OSSub U0);

        reconsider a2 = a1 as strict OSSubAlgebra of U0 by Def14;



        thus (G1 "/\" a) = (( GenOSAlg C) /\ a2) by Def16

        .= G1 by Th36;

        hence (a "/\" G1) = G1;

      end;

      hence thesis by LATTICES:def 16;

    end;

    theorem :: OSALG_2:50



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

      reconsider G = ( GenOSAlg B) as Element of ( OSSub U0) by Def14;

      set L = ( OSSubAlLattice U0);

      reconsider G1 = G as Element of L;

      assume

       A1: B = the Sorts of U0;

      now

        let a be Element of L;

        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;

        hence (a "\/" G1) = G1;

      end;

      hence thesis by LATTICES:def 17;

    end;

    theorem :: OSALG_2:51

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

    end;