closure3.miz



    begin

    registration

      let S be non empty 1-sorted;

      cluster the 1-sorted of S -> non empty;

      coherence ;

    end

    theorem :: CLOSURE3:1

    

     Th1: for I be non empty set, M,N be ManySortedSet of I holds (M +* N) = N

    proof

      let I be non empty set, M,N be ManySortedSet of I;

      ( dom M) = I by PARTFUN1:def 2

      .= ( dom N) by PARTFUN1:def 2;

      hence thesis by FUNCT_4: 19;

    end;

    theorem :: CLOSURE3:2

    for I be set, M,N be ManySortedSet of I, F be SubsetFamily of M holds N in F implies ( meet |:F:|) c=' N by CLOSURE2: 21, MSSUBFAM: 43;

    theorem :: CLOSURE3:3

    

     Th3: for S be non void non empty ManySortedSign, MA be strict non-empty MSAlgebra over S holds for F be SubsetFamily of the Sorts of MA st F c= ( SubSort MA) holds for B be MSSubset of MA st B = ( meet |:F:|) holds B is opers_closed

    proof

      let S be non void non empty ManySortedSign, MA be strict non-empty MSAlgebra over S;

      let F be SubsetFamily of the Sorts of MA such that

       A1: F c= ( SubSort MA);

      let B be MSSubset of MA such that

       A2: B = ( meet |:F:|);

      per cases ;

        suppose

         A3: F = {} ;

        set Q = the Sorts of MA;

        reconsider FF = |:F:| as MSSubsetFamily of the Sorts of MA;

        set I = the carrier of S;

        FF = ( EmptyMS I) by A3;

        then

         A4: Q = B by A2, MSSUBFAM: 41;

        reconsider Q as MSSubset of MA by PBOOLE:def 18;

        for o be OperSymbol of S holds Q is_closed_on o

        proof

          let o be OperSymbol of S;

          

           A5: (the ResultSort of S . o) = ( the_result_sort_of o) & ( dom the ResultSort of S) = the carrier' of S by FUNCT_2:def 1, MSUALG_1:def 2;

          ( Result (o,MA)) = ((Q * the ResultSort of S) . o) by MSUALG_1:def 5

          .= (Q . ( the_result_sort_of o)) by A5, FUNCT_1: 13;

          then

           A6: ( rng (( Den (o,MA)) | ((Q # ) . ( the_arity_of o)))) c= (Q . ( the_result_sort_of o)) by RELAT_1:def 19;

          (the Arity of S . o) = ( the_arity_of o) & ( dom the Arity of S) = the carrier' of S by FUNCT_2:def 1, MSUALG_1:def 1;

          then

           A7: (((Q # ) * the Arity of S) . o) = ((Q # ) . ( the_arity_of o)) by FUNCT_1: 13;

          ((Q * the ResultSort of S) . o) = (Q . ( the_result_sort_of o)) by A5, FUNCT_1: 13;

          hence thesis by A7, A6;

        end;

        hence thesis by A4;

      end;

        suppose

         A8: F <> {} ;

        set SS = S;

        let o be OperSymbol of SS;

        set i = ( the_result_sort_of o);

        

         A9: (the ResultSort of SS . o) = ( the_result_sort_of o) by MSUALG_1:def 2;

        

         A10: ( dom the ResultSort of SS) = the carrier' of SS by FUNCT_2:def 1;

        (the Arity of SS . o) = ( the_arity_of o) & ( dom the Arity of SS) = the carrier' of SS by FUNCT_2:def 1, MSUALG_1:def 1;

        then

         A11: (((B # ) * the Arity of SS) . o) = ((B # ) . ( the_arity_of o)) by FUNCT_1: 13;

        ( Result (o,MA)) = ((the Sorts of MA * the ResultSort of SS) . o) by MSUALG_1:def 5

        .= (the Sorts of MA . ( the_result_sort_of o)) by A9, A10, FUNCT_1: 13;

        then

         A12: ( rng (( Den (o,MA)) | ((B # ) . ( the_arity_of o)))) c= (the Sorts of MA . ( the_result_sort_of o)) by RELAT_1:def 19;

        

         A13: ( rng (( Den (o,MA)) | ((B # ) . ( the_arity_of o)))) c= (B . ( the_result_sort_of o))

        proof

          consider Q be Subset-Family of (the Sorts of MA . i) such that

           A14: Q = ( |:F:| . i) and

           A15: (B . i) = ( Intersect Q) by A2, MSSUBFAM:def 1;

          let v be object;

          assume

           A16: v in ( rng (( Den (o,MA)) | ((B # ) . ( the_arity_of o))));

          then

          consider p be object such that

           A17: p in ( dom (( Den (o,MA)) | ((B # ) . ( the_arity_of o)))) and

           A18: v = ((( Den (o,MA)) | ((B # ) . ( the_arity_of o))) . p) by FUNCT_1:def 3;

          for Y be set st Y in Q holds v in Y

          proof

            

             A19: ( |:F:| . i) = { (xx . i) where xx be Element of ( Bool the Sorts of MA) : xx in F } by A8, CLOSURE2: 14;

            let Y be set;

            assume Y in Q;

            then

            consider xx be Element of ( Bool the Sorts of MA) such that

             A20: Y = (xx . i) and

             A21: xx in F by A14, A19;

            reconsider xx as MSSubset of MA;

            xx is opers_closed by A1, A21, MSUALG_2: 14;

            then xx is_closed_on o;

            then

             A22: ( rng (( Den (o,MA)) | (((xx # ) * the Arity of SS) . o))) c= ((xx * the ResultSort of SS) . o);

            B c= xx by A2, A21, CLOSURE2: 21, MSSUBFAM: 43;

            then (( Den (o,MA)) | (((B # ) * the Arity of SS) . o)) c= (( Den (o,MA)) | (((xx # ) * the Arity of SS) . o)) by MSUALG_2: 2, RELAT_1: 75;

            then

             A23: ( dom (( Den (o,MA)) | (((B # ) * the Arity of SS) . o))) c= ( dom (( Den (o,MA)) | (((xx # ) * the Arity of SS) . o))) by RELAT_1: 11;

            

             A24: v = (( Den (o,MA)) . p) by A17, A18, FUNCT_1: 47;

            then v = ((( Den (o,MA)) | (((xx # ) * the Arity of SS) . o)) . p) by A11, A17, A23, FUNCT_1: 47;

            then v in ( rng (( Den (o,MA)) | (((xx # ) * the Arity of SS) . o))) by A11, A17, A23, FUNCT_1:def 3;

            then (( Den (o,MA)) . p) in ((xx * the ResultSort of SS) . o) by A22, A24;

            then (( Den (o,MA)) . p) in (xx . (the ResultSort of SS . o)) by A10, FUNCT_1: 13;

            then (( Den (o,MA)) . p) in (xx . i) by MSUALG_1:def 2;

            hence thesis by A17, A18, A20, FUNCT_1: 47;

          end;

          hence thesis by A12, A16, A15, SETFAM_1: 43;

        end;

        ((B * the ResultSort of SS) . o) = (B . ( the_result_sort_of o)) by A9, A10, FUNCT_1: 13;

        hence thesis by A11, A13;

      end;

    end;

    begin

    theorem :: CLOSURE3:4

    for A,B,C be set holds A is_coarser_than B & B is_coarser_than C implies A is_coarser_than C

    proof

      let A,B,C be set;

      assume that

       A1: A is_coarser_than B and

       A2: B is_coarser_than C;

      let a be set;

      assume a in A;

      then

      consider b be set such that

       A3: b in B and

       A4: b c= a by A1;

      consider c be set such that

       A5: c in C & c c= b by A2, A3;

      take c;

      thus thesis by A4, A5;

    end;

     Lm1:

    now

      let I be non empty set, M be ManySortedSet of I;

      set F = { x where x be Element of I : (M . x) <> {} };

      thus ( support M) = F

      proof

        thus ( support M) c= F

        proof

          let x be object;

          

           A1: ( dom M) = I by PARTFUN1:def 2;

          

           A2: ( support M) c= ( dom M) by PRE_POLY: 37;

          assume

           A3: x in ( support M);

          then (M . x) <> {} by PRE_POLY:def 7;

          hence thesis by A1, A2, A3;

        end;

        let x be object;

        assume x in F;

        then ex i be Element of I st x = i & (M . i) <> {} ;

        hence thesis by PRE_POLY:def 7;

      end;

    end;

    definition

      let I be non empty set, M be ManySortedSet of I;

      :: original: support

      redefine

      :: CLOSURE3:def1

      func support M equals { x where x be Element of I : (M . x) <> {} };

      compatibility by Lm1;

    end

    theorem :: CLOSURE3:5

    for I be non empty set, M be non-empty ManySortedSet of I holds M = (( EmptyMS I) +* (M | ( support M)))

    proof

      let I be non empty set, M be non-empty ManySortedSet of I;

      set MM = (M | ( support M));

      

       A1: I c= ( support M)

      proof

        let v be object;

        assume

         A2: v in I;

        then (M . v) <> {} ;

        hence thesis by A2;

      end;

      ( dom M) = I by PARTFUN1:def 2;

      then MM = M by A1, RELAT_1: 68;

      hence thesis by Th1;

    end;

    theorem :: CLOSURE3:6

    for I be non empty set, M1,M2 be non-empty ManySortedSet of I holds (M1 | ( support M1)) = (M2 | ( support M2)) implies M1 = M2

    proof

      let I be non empty set, M1,M2 be non-empty ManySortedSet of I;

      

       A1: ( dom M1) = I by PARTFUN1:def 2;

      

       A2: ( dom M2) = I by PARTFUN1:def 2;

      assume

       A3: (M1 | ( support M1)) = (M2 | ( support M2));

      for x be object st x in I holds (M1 . x) = (M2 . x)

      proof

        let x be object;

        

         A4: ( dom (M2 | ( support M2))) = (( dom M2) /\ ( support M2)) by RELAT_1: 61;

        assume

         A5: x in I;

        then (M1 . x) is non empty;

        then

         A6: x in ( support M1) by A5;

        (M2 . x) is non empty by A5;

        then x in ( support M2) by A5;

        then

         A7: x in ( dom (M2 | ( support M2))) by A2, A5, A4, XBOOLE_0:def 4;

        ( dom (M1 | ( support M1))) = (( dom M1) /\ ( support M1)) by RELAT_1: 61;

        then x in ( dom (M1 | ( support M1))) by A1, A5, A6, XBOOLE_0:def 4;

        

        then (M1 . x) = ((M2 | ( support M2)) . x) by A3, FUNCT_1: 47

        .= (M2 . x) by A7, FUNCT_1: 47;

        hence thesis;

      end;

      hence thesis;

    end;

    ::$Canceled

    theorem :: CLOSURE3:8

    

     Th7: for I be non empty set, M be ManySortedSet of I, x be Element of ( Bool M), i be Element of I holds for y be set st y in (x . i) holds ex a be Element of ( Bool M) st y in (a . i) & a is finite-yielding & ( support a) is finite & a c= x

    proof

      let I be non empty set, M be ManySortedSet of I, x be Element of ( Bool M), i be Element of I;

      let y be set such that

       A1: y in (x . i);

      set N = ( {i} --> {y});

      set A = (( EmptyMS I) +* N);

      

       A2: ( dom N) = {i} by FUNCOP_1: 13;

      then

       A3: i in ( dom N) by TARSKI:def 1;

      then

       A4: (N . i) = {y} by A2, FUNCOP_1: 7;

      then

       A5: (A . i) = {y} by A3, FUNCT_4: 13;

      

       A6: ( dom A) = (( dom ( EmptyMS I)) \/ ( dom N)) by FUNCT_4:def 1

      .= (I \/ {i}) by A2, PARTFUN1:def 2

      .= I by ZFMISC_1: 40;

      then

      reconsider A as ManySortedSet of I by PARTFUN1:def 2, RELAT_1:def 18;

      for j be object st j in I holds (A . j) c= (M . j)

      proof

        let j be object such that

         A7: j in I;

        per cases ;

          suppose

           A8: i = j;

          reconsider x as ManySortedSubset of M;

          let v be object;

          assume v in (A . j);

          then v in {y} by A3, A4, A8, FUNCT_4: 13;

          then

           A9: v in (x . j) by A1, A8, TARSKI:def 1;

          x c= M by PBOOLE:def 18;

          then (x . j) c= (M . j) by A7;

          hence thesis by A9;

        end;

          suppose i <> j;

          then

           A10: not j in {i} by TARSKI:def 1;

          j in (( dom ( EmptyMS I)) \/ ( dom N)) by A6, A7, FUNCT_4:def 1;

          

          then (A . j) = ((I --> {} ) . j) by A2, A10, FUNCT_4:def 1

          .= {} by A7, FUNCOP_1: 7;

          hence thesis;

        end;

      end;

      then A c= M;

      then

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

      reconsider a = AA as Element of ( Bool M) by CLOSURE2:def 1;

      

       A11: for j be object st j in I holds (a . j) c= (x . j)

      proof

        let j be object such that

         A12: j in I;

        per cases ;

          suppose

           A13: i = j;

          let v be object;

          assume

           A14: v in (a . j);

          (a . j) = {y} by A3, A4, A13, FUNCT_4: 13;

          hence thesis by A1, A13, A14, TARSKI:def 1;

        end;

          suppose j <> i;

          then

           A15: not j in {i} by TARSKI:def 1;

          j in (( dom ( EmptyMS I)) \/ ( dom N)) by A6, A12, FUNCT_4:def 1;

          

          then (a . j) = ((I --> {} ) . j) by A2, A15, FUNCT_4:def 1

          .= {} by A12, FUNCOP_1: 7;

          hence thesis;

        end;

      end;

      

       A16: { b where b be Element of I : (a . b) <> {} } = {i}

      proof

        thus { b where b be Element of I : (a . b) <> {} } c= {i}

        proof

          let s be object;

          assume s in { b where b be Element of I : (a . b) <> {} };

          then

           A17: ex b be Element of I st s = b & (a . b) <> {} ;

          assume

           A18: not s in {i};

          reconsider s as Element of I by A17;

          s in ( dom a) by A6;

          then s in (( dom ( EmptyMS I)) \/ ( dom N)) by FUNCT_4:def 1;

          

          then (a . s) = ((I --> {} ) . s) by A2, A18, FUNCT_4:def 1

          .= {} by FUNCOP_1: 7;

          hence contradiction by A17;

        end;

        let s be object;

        assume

         A19: s in {i};

        then

         A20: s = i by TARSKI:def 1;

        reconsider s as Element of I by A19, TARSKI:def 1;

        (a . s) = {y} by A3, A4, A20, FUNCT_4: 13;

        hence thesis;

      end;

      take a;

      for j be object st j in I holds (a . j) is finite

      proof

        let j be object such that

         A21: j in I;

        per cases ;

          suppose j = i;

          hence thesis by A3, A4, FUNCT_4: 13;

        end;

          suppose j <> i;

          then

           A22: not j in {i} by TARSKI:def 1;

          j in (( dom ( EmptyMS I)) \/ ( dom N)) by A6, A21, FUNCT_4:def 1;

          

          then (a . j) = ((I --> {} ) . j) by A2, A22, FUNCT_4:def 1

          .= {} by A21, FUNCOP_1: 7;

          hence thesis;

        end;

      end;

      hence thesis by A5, A16, A11, FINSET_1:def 5, TARSKI:def 1;

    end;

    definition

      let I be set, M be ManySortedSet of I;

      let A be SubsetFamily of M;

      :: CLOSURE3:def2

      func MSUnion A -> ManySortedSubset of M means

      : Def2: for i be set st i in I holds (it . i) = ( union { (f . i) where f be Element of ( Bool M) : f in A });

      existence

      proof

        defpred P[ object, object] means $2 = ( union { (f . $1) where f be Element of ( Bool M) : f in A });

        

         A1: for x be object st x in I holds ex y be object st P[x, y];

        consider IT be Function such that

         A2: ( dom IT) = I and

         A3: for x be object st x in I holds P[x, (IT . x)] from CLASSES1:sch 1( A1);

        reconsider IT as ManySortedSet of I by A2, PARTFUN1:def 2, RELAT_1:def 18;

        for i be object st i in I holds (IT . i) c= (M . i)

        proof

          let i be object such that

           A4: i in I;

          for x be object holds x in (IT . i) implies x in (M . i)

          proof

            let x be object;

            assume

             A5: x in (IT . i);

            (IT . i) = ( union { (f . i) where f be Element of ( Bool M) : f in A }) by A3, A4;

            then

            consider Y be set such that

             A6: x in Y and

             A7: Y in { (f . i) where f be Element of ( Bool M) : f in A } by A5, TARSKI:def 4;

            consider ff be Element of ( Bool M) such that

             A8: (ff . i) = Y and ff in A by A7;

            reconsider ff as ManySortedSubset of M;

            ff c= M by PBOOLE:def 18;

            then (ff . i) c= (M . i) by A4;

            hence thesis by A6, A8;

          end;

          hence thesis;

        end;

        then IT c= M;

        then

        reconsider IT as ManySortedSubset of M by PBOOLE:def 18;

        take IT;

        thus thesis by A3;

      end;

      uniqueness

      proof

        let B1,B2 be ManySortedSubset of M;

        assume that

         A9: for i be set st i in I holds (B1 . i) = ( union { (f . i) where f be Element of ( Bool M) : f in A }) and

         A10: for i be set st i in I holds (B2 . i) = ( union { (ff . i) where ff be Element of ( Bool M) : ff in A });

        for i be object st i in I holds (B1 . i) = (B2 . i)

        proof

          let i be object;

          assume

           A11: i in I;

          

          then (B1 . i) = ( union { (f . i) where f be Element of ( Bool M) : f in A }) by A9

          .= (B2 . i) by A10, A11;

          hence thesis;

        end;

        hence thesis;

      end;

    end

    registration

      let I be set, M be ManySortedSet of I, A be empty SubsetFamily of M;

      cluster ( MSUnion A) -> empty-yielding;

      coherence

      proof

        let i be object;

        set MA = ( MSUnion A);

        assume i in I;

        then

         A1: (MA . i) = ( union { (f . i) where f be Element of ( Bool M) : f in A }) by Def2;

        assume (MA . i) is non empty;

        then

        consider v be object such that

         A2: v in (MA . i);

        consider h be set such that v in h and

         A3: h in { (f . i) where f be Element of ( Bool M) : f in A } by A1, A2, TARSKI:def 4;

        ex g be Element of ( Bool M) st h = (g . i) & g in A by A3;

        hence contradiction;

      end;

    end

    theorem :: CLOSURE3:9

    for I be set, M be ManySortedSet of I, A be SubsetFamily of M holds ( MSUnion A) = ( union |:A:|)

    proof

      let I be set, M be ManySortedSet of I, A be SubsetFamily of M;

      set AA = |:A:|;

      reconsider UA = ( union AA) as ManySortedSet of I;

      per cases ;

        suppose

         A1: A is non empty;

        for i be object st i in I holds (( MSUnion A) . i) = (UA . i)

        proof

          let i be object;

          assume

           A2: i in I;

          then (AA . i) = { (g . i) where g be Element of ( Bool M) : g in A } & (UA . i) = ( union (AA . i)) by A1, CLOSURE2: 14, MBOOLEAN:def 2;

          hence thesis by A2, Def2;

        end;

        hence thesis;

      end;

        suppose

         A3: A is empty SubsetFamily of M;

        for i be object st i in I holds (( MSUnion A) . i) = (UA . i)

        proof

          let i be object;

          assume i in I;

          AA = ( EmptyMS I) by A3;

          then UA = ( EmptyMS I) by MBOOLEAN: 21;

          then (UA . i) is empty;

          hence thesis by A3;

        end;

        hence thesis;

      end;

    end;

    definition

      let I be set, M be ManySortedSet of I, A,B be SubsetFamily of M;

      :: original: \/

      redefine

      func A \/ B -> SubsetFamily of M ;

      correctness by CLOSURE2: 3;

    end

    theorem :: CLOSURE3:10

    for I be set, M be ManySortedSet of I holds for A,B be SubsetFamily of M holds ( MSUnion (A \/ B)) = (( MSUnion A) (\/) ( MSUnion B))

    proof

      let I be set, M be ManySortedSet of I, A,B be SubsetFamily of M;

      reconsider MAB = ( MSUnion (A \/ B)) as ManySortedSubset of M;

      reconsider MAB as ManySortedSet of I;

      reconsider MA = ( MSUnion A) as ManySortedSubset of M;

      reconsider MA as ManySortedSet of I;

      reconsider MB = ( MSUnion B) as ManySortedSubset of M;

      reconsider MB as ManySortedSet of I;

      for i be object st i in I holds (MAB . i) = ((MA (\/) MB) . i)

      proof

        let i be object;

        assume

         A1: i in I;

        then

         A2: (MAB . i) = ( union { (f . i) where f be Element of ( Bool M) : f in (A \/ B) }) by Def2;

        

         A3: ((MA (\/) MB) . i) = ((MA . i) \/ (MB . i)) by A1, PBOOLE:def 4;

        

         A4: for v be object holds v in ((MA (\/) MB) . i) implies v in (MAB . i)

        proof

          let v be object;

          assume v in ((MA (\/) MB) . i);

          then

           A5: v in (MA . i) or v in (MB . i) by A3, XBOOLE_0:def 3;

          per cases by A1, A5, Def2;

            suppose v in ( union { (f . i) where f be Element of ( Bool M) : f in A });

            then

            consider g be set such that

             A6: v in g and

             A7: g in { (f . i) where f be Element of ( Bool M) : f in A } by TARSKI:def 4;

            consider h be Element of ( Bool M) such that

             A8: g = (h . i) and

             A9: h in A by A7;

            h in (A \/ B) by A9, XBOOLE_0:def 3;

            then g in { (f . i) where f be Element of ( Bool M) : f in (A \/ B) } by A8;

            hence thesis by A2, A6, TARSKI:def 4;

          end;

            suppose v in ( union { (f . i) where f be Element of ( Bool M) : f in B });

            then

            consider g be set such that

             A10: v in g and

             A11: g in { (f . i) where f be Element of ( Bool M) : f in B } by TARSKI:def 4;

            consider h be Element of ( Bool M) such that

             A12: g = (h . i) and

             A13: h in B by A11;

            h in (A \/ B) by A13, XBOOLE_0:def 3;

            then g in { (f . i) where f be Element of ( Bool M) : f in (A \/ B) } by A12;

            hence thesis by A2, A10, TARSKI:def 4;

          end;

        end;

        

         A14: (MA . i) = ( union { (f . i) where f be Element of ( Bool M) : f in A }) & (MB . i) = ( union { (f . i) where f be Element of ( Bool M) : f in B }) by A1, Def2;

        for v be object holds v in (MAB . i) implies v in ((MA (\/) MB) . i)

        proof

          let v be object;

          assume v in (MAB . i);

          then

          consider h be set such that

           A15: v in h and

           A16: h in { (f . i) where f be Element of ( Bool M) : f in (A \/ B) } by A2, TARSKI:def 4;

          consider g be Element of ( Bool M) such that

           A17: h = (g . i) and

           A18: g in (A \/ B) by A16;

          g in A or g in B by A18, XBOOLE_0:def 3;

          then h in { (f . i) where f be Element of ( Bool M) : f in A } or h in { (f . i) where f be Element of ( Bool M) : f in B } by A17;

          then v in ( union { (f . i) where f be Element of ( Bool M) : f in A }) or v in ( union { (f . i) where f be Element of ( Bool M) : f in B }) by A15, TARSKI:def 4;

          hence thesis by A3, A14, XBOOLE_0:def 3;

        end;

        hence thesis by A4, TARSKI: 2;

      end;

      hence thesis;

    end;

    theorem :: CLOSURE3:11

    for I be set, M be ManySortedSet of I holds for A,B be SubsetFamily of M holds A c= B implies ( MSUnion A) c= ( MSUnion B)

    proof

      let I be set, M be ManySortedSet of I;

      let A,B be SubsetFamily of M;

      reconsider MA = ( MSUnion A) as ManySortedSubset of M;

      reconsider MA as ManySortedSet of I;

      reconsider MB = ( MSUnion B) as ManySortedSubset of M;

      reconsider MB as ManySortedSet of I;

      assume

       A1: A c= B;

      for i be object st i in I holds (MA . i) c= (MB . i)

      proof

        let i be object such that

         A2: i in I;

        for v be object st v in (MA . i) holds v in (MB . i)

        proof

          

           A3: (MA . i) = ( union { (f . i) where f be Element of ( Bool M) : f in A }) by A2, Def2;

          let v be object;

          assume v in (MA . i);

          then

          consider h be set such that

           A4: v in h and

           A5: h in { (f . i) where f be Element of ( Bool M) : f in A } by A3, TARSKI:def 4;

          ex g be Element of ( Bool M) st h = (g . i) & g in A by A5;

          then h in { (k . i) where k be Element of ( Bool M) : k in B } by A1;

          then v in ( union { (k . i) where k be Element of ( Bool M) : k in B }) by A4, TARSKI:def 4;

          hence thesis by A2, Def2;

        end;

        hence thesis;

      end;

      hence thesis;

    end;

    definition

      let I be set, M be ManySortedSet of I, A,B be SubsetFamily of M;

      :: original: /\

      redefine

      func A /\ B -> SubsetFamily of M ;

      correctness by CLOSURE2: 4;

    end

    theorem :: CLOSURE3:12

    for I be set, M be ManySortedSet of I holds for A,B be SubsetFamily of M holds ( MSUnion (A /\ B)) c= (( MSUnion A) (/\) ( MSUnion B))

    proof

      let I be set, M be ManySortedSet of I;

      let A,B be SubsetFamily of M;

      reconsider MAB = ( MSUnion (A /\ B)) as ManySortedSet of I;

      reconsider MA = ( MSUnion A) as ManySortedSet of I;

      reconsider MB = ( MSUnion B) as ManySortedSet of I;

      for i be object st i in I holds (MAB . i) c= ((MA (/\) MB) . i)

      proof

        let i be object;

        assume

         A1: i in I;

        then

         A2: (MA . i) = ( union { (f . i) where f be Element of ( Bool M) : f in A }) & (MB . i) = ( union { (f . i) where f be Element of ( Bool M) : f in B }) by Def2;

        

         A3: (MAB . i) = ( union { (f . i) where f be Element of ( Bool M) : f in (A /\ B) }) by A1, Def2;

        for v be object st v in (MAB . i) holds v in ((MA (/\) MB) . i)

        proof

          let v be object;

          assume v in (MAB . i);

          then

          consider w be set such that

           A4: v in w and

           A5: w in { (f . i) where f be Element of ( Bool M) : f in (A /\ B) } by A3, TARSKI:def 4;

          consider g be Element of ( Bool M) such that

           A6: w = (g . i) and

           A7: g in (A /\ B) by A5;

          g in B by A7, XBOOLE_0:def 4;

          then w in { (f . i) where f be Element of ( Bool M) : f in B } by A6;

          then

           A8: v in ( union { (f . i) where f be Element of ( Bool M) : f in B }) by A4, TARSKI:def 4;

          g in A by A7, XBOOLE_0:def 4;

          then w in { (f . i) where f be Element of ( Bool M) : f in A } by A6;

          then v in ( union { (f . i) where f be Element of ( Bool M) : f in A }) by A4, TARSKI:def 4;

          then v in ((MA . i) /\ (MB . i)) by A2, A8, XBOOLE_0:def 4;

          hence thesis by A1, PBOOLE:def 5;

        end;

        hence thesis;

      end;

      hence thesis;

    end;

    theorem :: CLOSURE3:13

    for I be set, M be ManySortedSet of I, AA be set st for x be set st x in AA holds x is SubsetFamily of M holds for A,B be SubsetFamily of M st B = { ( MSUnion X) where X be SubsetFamily of M : X in AA } & A = ( union AA) holds ( MSUnion B) = ( MSUnion A)

    proof

      let I be set, M be ManySortedSet of I, AA be set such that

       A1: for x be set st x in AA holds x is SubsetFamily of M;

      let A,B be SubsetFamily of M such that

       A2: B = { ( MSUnion X) where X be SubsetFamily of M : X in AA } and

       A3: A = ( union AA);

      let i be object such that

       A4: i in I;

      thus (( MSUnion B) . i) c= (( MSUnion A) . i)

      proof

        let a be object;

        thus a in (( MSUnion B) . i) implies a in (( MSUnion A) . i)

        proof

          assume a in (( MSUnion B) . i);

          then a in ( union { (f . i) where f be Element of ( Bool M) : f in B }) by A4, Def2;

          then

          consider Y be set such that

           A5: a in Y and

           A6: Y in { (f . i) where f be Element of ( Bool M) : f in B } by TARSKI:def 4;

          consider f be Element of ( Bool M) such that

           A7: (f . i) = Y and

           A8: f in B by A6;

          consider Q be SubsetFamily of M such that

           A9: f = ( MSUnion Q) and

           A10: Q in AA by A2, A8;

          (( MSUnion Q) . i) = ( union { (g . i) where g be Element of ( Bool M) : g in Q }) by A4, Def2;

          then

          consider d be set such that

           A11: a in d and

           A12: d in { (g . i) where g be Element of ( Bool M) : g in Q } by A5, A7, A9, TARSKI:def 4;

          consider g be Element of ( Bool M) such that

           A13: d = (g . i) and

           A14: g in Q by A12;

          g in ( union AA) by A10, A14, TARSKI:def 4;

          then d in { (h . i) where h be Element of ( Bool M) : h in ( union AA) } by A13;

          then a in ( union { (h . i) where h be Element of ( Bool M) : h in ( union AA) }) by A11, TARSKI:def 4;

          hence thesis by A3, A4, Def2;

        end;

      end;

      let a be object;

      assume a in (( MSUnion A) . i);

      then a in ( union { (f . i) where f be Element of ( Bool M) : f in A }) by A4, Def2;

      then

      consider Y be set such that

       A15: a in Y and

       A16: Y in { (f . i) where f be Element of ( Bool M) : f in A } by TARSKI:def 4;

      consider f be Element of ( Bool M) such that

       A17: (f . i) = Y and

       A18: f in A by A16;

      consider c be set such that

       A19: f in c and

       A20: c in AA by A3, A18, TARSKI:def 4;

      reconsider c as SubsetFamily of M by A1, A20;

      (f . i) in { (v . i) where v be Element of ( Bool M) : v in c } by A19;

      then

       A21: a in ( union { (v . i) where v be Element of ( Bool M) : v in c }) by A15, A17, TARSKI:def 4;

      (( MSUnion c) . i) = ( union { (v . i) where v be Element of ( Bool M) : v in c }) by A4, Def2;

      then

      consider cos be set such that

       A22: a in cos and

       A23: cos = (( MSUnion c) . i) by A21;

      ( MSUnion c) in { ( MSUnion X) where X be SubsetFamily of M : X in AA } by A20;

      then cos in { (t . i) where t be Element of ( Bool M) : t in B } by A2, A23;

      then a in ( union { (t . i) where t be Element of ( Bool M) : t in B }) by A22, TARSKI:def 4;

      hence thesis by A4, Def2;

    end;

    begin

    definition

      let I be non empty set, M be ManySortedSet of I, S be SetOp of M;

      :: CLOSURE3:def3

      attr S is algebraic means for x be Element of ( Bool M) st x = (S . x) holds ex A be SubsetFamily of M st A = { (S . a) where a be Element of ( Bool M) : a is finite-yielding & ( support a) is finite & a c= x } & x = ( MSUnion A);

    end

    registration

      let I be non empty set, M be ManySortedSet of I;

      cluster algebraic reflexive monotonic idempotent for SetOp of M;

      existence

      proof

        reconsider f = ( id ( Bool M)) as SetOp of M;

        take f;

        thus f is algebraic

        proof

          let x be Element of ( Bool M) such that x = (f . x);

          set A = { (f . a) where a be Element of ( Bool M) : a is finite-yielding & ( support a) is finite & a c= x };

          A c= ( Bool M)

          proof

            let v be object;

            assume v in A;

            then ex a be Element of ( Bool M) st v = (f . a) & a is finite-yielding & ( support a) is finite & a c= x;

            hence thesis;

          end;

          then

          reconsider A as SubsetFamily of M;

          take A;

          thus A = { (f . a) where a be Element of ( Bool M) : a is finite-yielding & ( support a) is finite & a c= x };

          let i be Element of I;

          thus (x . i) c= (( MSUnion A) . i)

          proof

            let y be object;

            assume y in (x . i);

            then

            consider a be Element of ( Bool M) such that

             A1: y in (a . i) and

             A2: a is finite-yielding & ( support a) is finite & a c= x by Th7;

            a = (f . a);

            then a in A by A2;

            then (a . i) in { (g . i) where g be Element of ( Bool M) : g in A };

            then y in ( union { (g . i) where g be Element of ( Bool M) : g in A }) by A1, TARSKI:def 4;

            hence thesis by Def2;

          end;

          let v be object;

          assume v in (( MSUnion A) . i);

          then v in ( union { (ff . i) where ff be Element of ( Bool M) : ff in A }) by Def2;

          then

          consider Y be set such that

           A3: v in Y and

           A4: Y in { (ff . i) where ff be Element of ( Bool M) : ff in A } by TARSKI:def 4;

          consider ff be Element of ( Bool M) such that

           A5: Y = (ff . i) and

           A6: ff in A by A4;

          consider a be Element of ( Bool M) such that

           A7: ff = (f . a) and a is finite-yielding and ( support a) is finite and

           A8: a c= x by A6;

          ff = a by A7;

          then (ff . i) c= (x . i) by A8;

          hence thesis by A3, A5;

        end;

        thus f is reflexive;

        thus f is monotonic;

        thus f is idempotent;

      end;

    end

    definition

      let S be non empty 1-sorted, IT be ClosureSystem of S;

      :: CLOSURE3:def4

      attr IT is algebraic means ( ClSys->ClOp IT) is algebraic;

    end

    definition

      let S be non void non empty ManySortedSign, MA be non-empty MSAlgebra over S;

      :: CLOSURE3:def5

      func SubAlgCl MA -> strict ClosureStr over the 1-sorted of S means

      : Def5: the Sorts of it = the Sorts of MA & the Family of it = ( SubSort MA);

      existence

      proof

        reconsider SS = the Sorts of MA as ManySortedSet of the carrier of the 1-sorted of S;

        ( SubSort MA) c= ( Bool the Sorts of MA)

        proof

          let x be object;

          assume x in ( SubSort MA);

          then x is ManySortedSubset of the Sorts of MA by MSUALG_2:def 11;

          hence thesis by CLOSURE2:def 1;

        end;

        then

        reconsider SF = ( SubSort MA) as SubsetFamily of SS;

        take ClosureStr (# SS, SF #);

        thus thesis;

      end;

      uniqueness ;

    end

    theorem :: CLOSURE3:14

    

     Th13: for S be non void non empty ManySortedSign, MA be strict non-empty MSAlgebra over S holds ( SubSort MA) is absolutely-multiplicative SubsetFamily of the Sorts of MA

    proof

      let S be non void non empty ManySortedSign, MA be strict non-empty MSAlgebra over S;

      ( SubSort MA) c= ( Bool the Sorts of MA)

      proof

        let x be object;

        assume x in ( SubSort MA);

        then x is ManySortedSubset of the Sorts of MA by MSUALG_2:def 11;

        hence thesis by CLOSURE2:def 1;

      end;

      then

      reconsider SUBMA = ( SubSort MA) as SubsetFamily of the Sorts of MA;

      for F be SubsetFamily of the Sorts of MA st F c= SUBMA holds ( meet |:F:|) in SUBMA

      proof

        set M = ( bool ( Union the Sorts of MA));

        set I = the carrier of S;

        let F be SubsetFamily of the Sorts of MA such that

         A1: F c= SUBMA;

        set x = ( meet |:F:|);

        

         A2: ( dom x) = I by PARTFUN1:def 2;

        ( rng x) c= M

        proof

          let u be object;

          reconsider uu = u as set by TARSKI: 1;

          assume u in ( rng x);

          then

          consider i be object such that

           A3: i in ( dom x) and

           A4: u = (x . i) by FUNCT_1:def 3;

          ( dom the Sorts of MA) = I by PARTFUN1:def 2;

          then (the Sorts of MA . i) in ( rng the Sorts of MA) by A2, A3, FUNCT_1:def 3;

          then

           A5: (the Sorts of MA . i) c= ( union ( rng the Sorts of MA)) by ZFMISC_1: 74;

          ex Q be Subset-Family of (the Sorts of MA . i) st Q = ( |:F:| . i) & u = ( Intersect Q) by A2, A3, A4, MSSUBFAM:def 1;

          then uu c= ( union ( rng the Sorts of MA)) by A5;

          then u in ( bool ( union ( rng the Sorts of MA)));

          hence thesis by CARD_3:def 4;

        end;

        then

         A6: x in ( Funcs (I,M)) by A2, FUNCT_2:def 2;

        reconsider x as MSSubset of MA;

        for B be MSSubset of MA st B = x holds B is opers_closed by A1, Th3;

        hence thesis by A6, MSUALG_2:def 11;

      end;

      hence thesis by CLOSURE2:def 7;

    end;

    registration

      let S be non void non empty ManySortedSign, MA be strict non-empty MSAlgebra over S;

      cluster ( SubAlgCl MA) -> absolutely-multiplicative;

      coherence

      proof

        thus ( SubAlgCl MA) is absolutely-multiplicative

        proof

          reconsider SF = ( SubSort MA) as absolutely-multiplicative SubsetFamily of the Sorts of MA by Th13;

          set F = the Family of ( SubAlgCl MA);

          the Sorts of ( SubAlgCl MA) = the Sorts of MA & F = SF by Def5;

          hence thesis;

        end;

      end;

    end

    registration

      let S be non void non empty ManySortedSign, MA be strict non-empty MSAlgebra over S;

      cluster ( SubAlgCl MA) -> algebraic;

      coherence

      proof

        set I = the carrier of S;

        set SS = ( ClSys->ClOp ( SubAlgCl MA)), M = the Sorts of ( SubAlgCl MA);

        let x be Element of ( Bool M) such that

         A1: x = (SS . x);

        set A = { (SS . a) where a be Element of ( Bool M) : a is finite-yielding & ( support a) is finite & a c= x };

        A c= ( Bool M)

        proof

          let v be object;

          assume v in A;

          then ex a be Element of ( Bool M) st v = (SS . a) & a is finite-yielding & ( support a) is finite & a c= x;

          then

          reconsider vv = v as Element of ( Bool M);

          vv in ( Bool M);

          hence thesis;

        end;

        then

        reconsider A as SubsetFamily of M;

        take A;

        thus A = { (SS . b) where b be Element of ( Bool M) : b is finite-yielding & ( support b) is finite & b c= x };

        reconsider y = x, z = ( MSUnion A) as ManySortedSet of I;

        y = z

        proof

          let i be Element of I;

          reconsider SS9 = SS as reflexive SetOp of M;

          thus (y . i) c= (z . i)

          proof

            let v be object;

            assume v in (y . i);

            then

            consider b be Element of ( Bool M) such that

             A2: v in (b . i) and

             A3: b is finite-yielding & ( support b) is finite & b c= x by Th7;

            b c=' (SS9 . b) by CLOSURE2:def 10;

            then

             A4: (b . i) c= ((SS9 . b) . i);

            (SS . b) in A by A3;

            then ((SS9 . b) . i) in { (f . i) where f be Element of ( Bool M) : f in A };

            then v in ( union { (f . i) where f be Element of ( Bool M) : f in A }) by A2, A4, TARSKI:def 4;

            hence thesis by Def2;

          end;

          reconsider SS9 = SS as monotonic SetOp of M;

          let v be object;

          assume v in (z . i);

          then v in ( union { (ff . i) where ff be Element of ( Bool M) : ff in A }) by Def2;

          then

          consider Y be set such that

           A5: v in Y and

           A6: Y in { (ff . i) where ff be Element of ( Bool M) : ff in A } by TARSKI:def 4;

          consider ff be Element of ( Bool M) such that

           A7: Y = (ff . i) and

           A8: ff in A by A6;

          consider a be Element of ( Bool M) such that

           A9: ff = (SS . a) and a is finite-yielding and ( support a) is finite and

           A10: a c=' x by A8;

          (SS9 . a) c=' (SS9 . x) by A10, CLOSURE2:def 11;

          then (ff . i) c= (x . i) by A1, A9;

          hence thesis by A5, A7;

        end;

        hence thesis;

      end;

    end