closure1.miz



    begin

    reserve i,x,I for set,

A,M for ManySortedSet of I,

f for Function,

F for ManySortedFunction of I;

    scheme :: CLOSURE1:sch1

    MSSUBSET { I() -> set , A() -> non-empty ManySortedSet of I() , B() -> ManySortedSet of I() , P[ set] } :

(for X be ManySortedSet of I() holds X in A() iff X in B() & P[X]) implies A() c= B();

      assume

       A1: for X be ManySortedSet of I() holds X in A() iff X in B() & P[X];

      consider K be ManySortedSet of I() such that

       A2: K in A() by PBOOLE: 134;

      let i be object such that

       A3: i in I();

      let x be object such that

       A4: x in (A() . i);

      ( dom (K +* (i .--> x))) = I() by A3, PZFMISC1: 1;

      then

      reconsider X = (K +* (i .--> x)) as ManySortedSet of I() by PARTFUN1:def 2, RELAT_1:def 18;

      

       A5: ( dom (i .--> x)) = {i};

      i in {i} by TARSKI:def 1;

      

      then

       A6: (X . i) = ((i .--> x) . i) by A5, FUNCT_4: 13

      .= x by FUNCOP_1: 72;

      X in A()

      proof

        let s be object such that

         A7: s in I();

        per cases ;

          suppose s = i;

          hence thesis by A4, A6;

        end;

          suppose s <> i;

          then not s in ( dom (i .--> x)) by TARSKI:def 1;

          then (X . s) = (K . s) by FUNCT_4: 11;

          hence thesis by A2, A7;

        end;

      end;

      then X in B() by A1;

      hence thesis by A3, A6;

    end;

    theorem :: CLOSURE1:1

    

     Th1: for X be non empty set holds for x,y be set st x c= y holds { t where t be Element of X : y c= t } c= { z where z be Element of X : x c= z }

    proof

      let X be non empty set, x,y be set such that

       A1: x c= y;

      let a be object;

      reconsider aa = a as set by TARSKI: 1;

      assume a in { t where t be Element of X : y c= t };

      then

       A2: ex b be Element of X st b = a & y c= b;

      then x c= aa by A1;

      hence thesis by A2;

    end;

    theorem :: CLOSURE1:2

    (ex A st A in M) implies M is non-empty;

    registration

      let I, F, A;

      cluster (F .. A) -> total;

      coherence ;

    end

     Lm1:

    now

      let I;

      let A,B be non-empty ManySortedSet of I;

      let F be ManySortedFunction of A, B;

      let X be Element of A;

      thus (F .. X) is Element of B

      proof

        let i be object such that

         A1: i in I;

        reconsider g = (F . i) as Function;

        g is Function of (A . i), (B . i) & (X . i) is Element of (A . i) by A1, PBOOLE:def 14, PBOOLE:def 15;

        then ( dom F) = I & (g . (X . i)) in (B . i) by A1, FUNCT_2: 5, PARTFUN1:def 2;

        hence thesis by A1, PRALG_1:def 20;

      end;

    end;

    definition

      let I;

      let A,B be non-empty ManySortedSet of I;

      let F be ManySortedFunction of A, B;

      let X be Element of A;

      :: original: ..

      redefine

      func F .. X -> Element of B ;

      coherence by Lm1;

    end

    theorem :: CLOSURE1:3

    for A,X be ManySortedSet of I holds for B be non-empty ManySortedSet of I holds for F be ManySortedFunction of A, B st X in A holds (F .. X) in B

    proof

      let A,X be ManySortedSet of I;

      let B be non-empty ManySortedSet of I;

      let F be ManySortedFunction of A, B such that

       A1: X in A;

      let i be object such that

       A2: i in I;

      reconsider g = (F . i) as Function;

      

       A3: g is Function of (A . i), (B . i) by A2, PBOOLE:def 15;

      (X . i) in (A . i) by A1, A2;

      then ( dom F) = I & (g . (X . i)) in (B . i) by A2, A3, FUNCT_2: 5, PARTFUN1:def 2;

      hence thesis by A2, PRALG_1:def 20;

    end;

    theorem :: CLOSURE1:4

    

     Th4: for F,G be ManySortedFunction of I holds for A be ManySortedSet of I st A in ( doms G) holds (F .. (G .. A)) = ((F ** G) .. A)

    proof

      let F,G be ManySortedFunction of I;

      reconsider FG = (F ** G) as ManySortedFunction of I by MSSUBFAM: 15;

      

       A3: ( dom FG) = I by PARTFUN1:def 2;

      let A be ManySortedSet of I such that

       A4: A in ( doms G);

       A5:

      now

        let i be object;

        reconsider f = (F . i) as Function;

        reconsider g = (G . i) as Function;

        reconsider fg = ((F ** G) . i) as Function;

        assume

         A6: i in I;

        then ( dom g) = (( doms G) . i) by MSSUBFAM: 14;

        then

         A7: (A . i) in ( dom g) by A4, A6;

        ((G .. A) . i) = (g . (A . i)) by A6, PRALG_1:def 20;

        

        hence ((F .. (G .. A)) . i) = (f . (g . (A . i))) by A6, PRALG_1:def 20

        .= ((f * g) . (A . i)) by A7, FUNCT_1: 13

        .= (fg . (A . i)) by A3, A6, PBOOLE:def 19

        .= (((F ** G) .. A) . i) by A3, A6, PRALG_1:def 20;

      end;

      (FG .. A) is ManySortedSet of I;

      hence thesis by A5, PBOOLE: 3;

    end;

    theorem :: CLOSURE1:5

    F is "1-1" implies for A,B be ManySortedSet of I st A in ( doms F) & B in ( doms F) & (F .. A) = (F .. B) holds A = B

    proof

      assume

       A1: F is "1-1";

      let A,B be ManySortedSet of I such that

       A2: A in ( doms F) & B in ( doms F) and

       A3: (F .. A) = (F .. B);

      now

        let i be object such that

         A4: i in I;

        reconsider f = (F . i) as Function;

        

         A5: f is one-to-one by A1, A4, MSUALG_3: 1;

        ( dom f) = (( doms F) . i) by A4, MSSUBFAM: 14;

        then

         A6: (A . i) in ( dom f) & (B . i) in ( dom f) by A2, A4;

        (f . (A . i)) = ((F .. A) . i) by A4, PRALG_1:def 20

        .= (f . (B . i)) by A3, A4, PRALG_1:def 20;

        hence (A . i) = (B . i) by A5, A6;

      end;

      hence thesis;

    end;

    theorem :: CLOSURE1:6

    ( doms F) is non-empty & (for A,B be ManySortedSet of I st A in ( doms F) & B in ( doms F) & (F .. A) = (F .. B) holds A = B) implies F is "1-1"

    proof

      assume that

       A1: ( doms F) is non-empty and

       A2: for A,B be ManySortedSet of I st A in ( doms F) & B in ( doms F) & (F .. A) = (F .. B) holds A = B;

      consider K be ManySortedSet of I such that

       A3: K in ( doms F) by A1, PBOOLE: 134;

      let i be set, f be Function such that

       A4: i in ( dom F) and

       A5: (F . i) = f;

      let x1,x2 be object such that

       A6: x1 in ( dom f) and

       A7: x2 in ( dom f) and

       A8: (f . x1) = (f . x2);

      

       A9: ( dom F) = I by PARTFUN1:def 2;

      then ( dom (K +* (i .--> x1))) = I by A4, PZFMISC1: 1;

      then

      reconsider X1 = (K +* (i .--> x1)) as ManySortedSet of I by PARTFUN1:def 2, RELAT_1:def 18;

      

       A10: ( dom (i .--> x1)) = {i};

      i in {i} by TARSKI:def 1;

      

      then

       A11: (X1 . i) = ((i .--> x1) . i) by A10, FUNCT_4: 13

      .= x1 by FUNCOP_1: 72;

      

       A12: X1 in ( doms F)

      proof

        let s be object such that

         A13: s in I;

        per cases ;

          suppose s = i;

          hence thesis by A5, A6, A11, A13, MSSUBFAM: 14;

        end;

          suppose s <> i;

          then not s in ( dom (i .--> x1)) by TARSKI:def 1;

          then (X1 . s) = (K . s) by FUNCT_4: 11;

          hence thesis by A3, A13;

        end;

      end;

      ( dom (K +* (i .--> x2))) = I by A4, A9, PZFMISC1: 1;

      then

      reconsider X2 = (K +* (i .--> x2)) as ManySortedSet of I by PARTFUN1:def 2, RELAT_1:def 18;

      

       A14: ( dom (i .--> x2)) = {i};

      i in {i} by TARSKI:def 1;

      

      then

       A15: (X2 . i) = ((i .--> x2) . i) by A14, FUNCT_4: 13

      .= x2 by FUNCOP_1: 72;

      

       A16: X2 in ( doms F)

      proof

        let s be object such that

         A17: s in I;

        per cases ;

          suppose s = i;

          hence thesis by A5, A7, A15, A17, MSSUBFAM: 14;

        end;

          suppose s <> i;

          then not s in ( dom (i .--> x2)) by TARSKI:def 1;

          then (X2 . s) = (K . s) by FUNCT_4: 11;

          hence thesis by A3, A17;

        end;

      end;

      now

        let s be object such that

         A18: s in I;

        per cases ;

          suppose

           A19: s = i;

          

           B1: s in ( dom F) by A18, PARTFUN1:def 2;

          

           B2: s in ( dom X2) & s in ( dom X1) by A18, PARTFUN1:def 2;

          then s in (( dom F) /\ ( dom X2)) by B1, XBOOLE_0:def 4;

          then

           a20: s in ( dom (F .. X2)) by PRALG_1:def 19;

          s in (( dom F) /\ ( dom X1)) by B1, B2, XBOOLE_0:def 4;

          then s in ( dom (F .. X1)) by PRALG_1:def 19;

          

          hence ((F .. X1) . s) = (f . (X2 . s)) by A5, A8, A11, A15, A19, PRALG_1:def 19

          .= ((F .. X2) . s) by A5, A19, PRALG_1:def 19, a20;

        end;

          suppose

           A20: s <> i;

          then not s in ( dom (i .--> x2)) by TARSKI:def 1;

          then

           A21: (X2 . s) = (K . s) by FUNCT_4: 11;

          reconsider f1 = (F . s) as Function;

          

           A22: not s in ( dom (i .--> x1)) by A20, TARSKI:def 1;

          

          thus ((F .. X1) . s) = (f1 . (X1 . s)) by A18, PRALG_1:def 20

          .= (f1 . (X2 . s)) by A22, A21, FUNCT_4: 11

          .= ((F .. X2) . s) by A18, PRALG_1:def 20;

        end;

      end;

      hence thesis by A2, A11, A15, A12, A16, PBOOLE: 3;

    end;

    theorem :: CLOSURE1:7

    

     Th7: for A,B be non-empty ManySortedSet of I holds for F,G be ManySortedFunction of A, B st for M st M in A holds (F .. M) = (G .. M) holds F = G

    proof

      let A,B be non-empty ManySortedSet of I, F,G be ManySortedFunction of A, B such that

       A1: for M st M in A holds (F .. M) = (G .. M);

      now

        let i be object;

        assume

         A2: i in I;

        then

        reconsider f = (F . i) as Function of (A . i), (B . i) by PBOOLE:def 15;

        reconsider g = (G . i) as Function of (A . i), (B . i) by A2, PBOOLE:def 15;

        now

          consider K be ManySortedSet of I such that

           A4: K in A by PBOOLE: 134;

          let x be object such that

           A5: x in (A . i);

          ( dom (K +* (i .--> x))) = I by A2, PZFMISC1: 1;

          then

          reconsider X = (K +* (i .--> x)) as ManySortedSet of I by PARTFUN1:def 2, RELAT_1:def 18;

          

           A6: ( dom (i .--> x)) = {i};

          i in {i} by TARSKI:def 1;

          

          then

           A7: (X . i) = ((i .--> x) . i) by A6, FUNCT_4: 13

          .= x by FUNCOP_1: 72;

          X in A

          proof

            let s be object such that

             A8: s in I;

            per cases ;

              suppose s = i;

              hence thesis by A5, A7;

            end;

              suppose s <> i;

              then not s in ( dom (i .--> x)) by TARSKI:def 1;

              then (X . s) = (K . s) by FUNCT_4: 11;

              hence thesis by A4, A8;

            end;

          end;

          then

           A9: (F .. X) = (G .. X) by A1;

          

          thus (f . x) = ((F .. X) . i) by A2, A7, PRALG_1:def 20

          .= (g . x) by A2, A7, A9, PRALG_1:def 20;

        end;

        hence (F . i) = (G . i) by FUNCT_2: 12;

      end;

      hence thesis;

    end;

    registration

      let I, M;

      cluster empty-yielding finite-yielding for Element of ( bool M);

      existence

      proof

        ( EmptyMS I) c= M by MBOOLEAN: 5;

        then ( EmptyMS I) in ( bool M) by MBOOLEAN: 1;

        then

        reconsider a = ( EmptyMS I) as Element of ( bool M) by MSSUBFAM: 11;

        take a;

        thus thesis;

      end;

    end

    begin

    definition

      let I, M;

      mode MSSetOp of M is ManySortedFunction of ( bool M), ( bool M);

    end

    definition

      let I, M;

      let O be MSSetOp of M;

      let X be Element of ( bool M);

      :: original: ..

      redefine

      func O .. X -> Element of ( bool M) ;

      coherence by Lm1;

    end

    definition

      let I, M;

      let IT be MSSetOp of M;

      :: CLOSURE1:def1

      attr IT is reflexive means

      : Def1: for X be Element of ( bool M) holds X c= (IT .. X);

      :: CLOSURE1:def2

      attr IT is monotonic means for X,Y be Element of ( bool M) st X c= Y holds (IT .. X) c= (IT .. Y);

      :: CLOSURE1:def3

      attr IT is idempotent means for X be Element of ( bool M) holds (IT .. X) = (IT .. (IT .. X));

      :: CLOSURE1:def4

      attr IT is topological means for X,Y be Element of ( bool M) holds (IT .. (X (\/) Y)) = ((IT .. X) (\/) (IT .. Y));

    end

    theorem :: CLOSURE1:8

    

     Th8: for M be non-empty ManySortedSet of I holds for X be Element of M holds X = (( id M) .. X)

    proof

      let M be non-empty ManySortedSet of I;

      let X be Element of M;

      set F = ( id M);

      now

        let i be object;

        reconsider g = (F . i) as Function;

        assume

         A2: i in I;

        then (X . i) is Element of (M . i) & (F . i) = ( id (M . i)) by MSUALG_3:def 1, PBOOLE:def 14;

        then (g . (X . i)) = (X . i);

        hence (X . i) = ((F .. X) . i) by A2, PRALG_1:def 20;

      end;

      hence thesis;

    end;

    theorem :: CLOSURE1:9

    

     Th9: for M be non-empty ManySortedSet of I holds for X,Y be Element of M st X c= Y holds (( id M) .. X) c= (( id M) .. Y)

    proof

      let M be non-empty ManySortedSet of I;

      let X,Y be Element of M such that

       A1: X c= Y;

      (( id M) .. X) = X by Th8;

      hence thesis by A1, Th8;

    end;

    theorem :: CLOSURE1:10

    

     Th10: for M be non-empty ManySortedSet of I holds for X,Y be Element of M st (X (\/) Y) is Element of M holds (( id M) .. (X (\/) Y)) = ((( id M) .. X) (\/) (( id M) .. Y))

    proof

      let M be non-empty ManySortedSet of I;

      let X,Y be Element of M;

      set F = ( id M);

      assume (X (\/) Y) is Element of M;

      

      hence (F .. (X (\/) Y)) = (X (\/) Y) by Th8

      .= ((F .. X) (\/) Y) by Th8

      .= ((F .. X) (\/) (F .. Y)) by Th8;

    end;

    theorem :: CLOSURE1:11

    for X be Element of ( bool M) holds for i,x be set st i in I & x in ((( id ( bool M)) .. X) . i) holds ex Y be finite-yielding Element of ( bool M) st Y c= X & x in ((( id ( bool M)) .. Y) . i)

    proof

      let X be Element of ( bool M), i,x be set such that

       A1: i in I and

       A2: x in ((( id ( bool M)) .. X) . i);

      

       A3: x in (X . i) by A2, Th8;

      set Y = ((I --> {} ) +* (i .--> {x}));

      ( dom Y) = I by A1, PZFMISC1: 1;

      then

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

      

       A4: ( dom (i .--> {x})) = {i};

      i in {i} by TARSKI:def 1;

      

      then

       A5: (Y . i) = ((i .--> {x}) . i) by A4, FUNCT_4: 13

      .= {x} by FUNCOP_1: 72;

      X in ( bool M) by MSSUBFAM: 12;

      then X c= M by MBOOLEAN: 18;

      then

       A6: (X . i) c= (M . i) by A1;

      Y is Element of ( bool M)

      proof

        let j be object such that

         A7: j in I;

        now

          per cases ;

            case

             A8: j = i;

            then {x} c= (M . j) by A3, A6, ZFMISC_1: 31;

            hence thesis by A5, A7, A8, MBOOLEAN:def 1;

          end;

            case j <> i;

            then not j in ( dom (i .--> {x})) by TARSKI:def 1;

            then (Y . j) = ((I --> {} ) . j) by FUNCT_4: 11;

            then (Y . j) = {} ;

            then (Y . j) c= (M . j);

            hence thesis by A7, MBOOLEAN:def 1;

          end;

        end;

        hence thesis;

      end;

      then

      reconsider Y as Element of ( bool M);

      Y is finite-yielding

      proof

        let j be object such that j in I;

        now

          per cases ;

            case j = i;

            hence thesis by A5;

          end;

            case j <> i;

            then not j in ( dom (i .--> {x})) by TARSKI:def 1;

            then (Y . j) = ((I --> {} ) . j) by FUNCT_4: 11;

            hence thesis;

          end;

        end;

        hence thesis;

      end;

      then

      reconsider Y as finite-yielding Element of ( bool M);

      take Y;

      thus Y c= X

      proof

        let j be object such that j in I;

        now

          per cases ;

            case j = i;

            hence thesis by A3, A5, ZFMISC_1: 31;

          end;

            case j <> i;

            then not j in ( dom (i .--> {x})) by TARSKI:def 1;

            then (Y . j) = ((I --> {} ) . j) by FUNCT_4: 11;

            then (Y . j) = {} ;

            hence thesis;

          end;

        end;

        hence thesis;

      end;

      x in (Y . i) by A5, TARSKI:def 1;

      hence thesis by Th8;

    end;

    registration

      let I, M;

      cluster reflexive monotonic idempotent topological for MSSetOp of M;

      existence

      proof

        reconsider F = ( id ( bool M)) as MSSetOp of M;

        take F;

        thus F is reflexive by Th8;

        thus F is monotonic by Th9;

        thus F is idempotent by Th8;

        thus F is topological

        proof

          let X,Y be Element of ( bool M);

          Y in ( bool M) by MSSUBFAM: 12;

          then

           A1: Y c= M by MBOOLEAN: 1;

          X in ( bool M) by MSSUBFAM: 12;

          then X c= M by MBOOLEAN: 1;

          then (X (\/) Y) c= M by A1, PBOOLE: 16;

          then (X (\/) Y) in ( bool M) by MBOOLEAN: 1;

          then (X (\/) Y) is Element of ( bool M) by MSSUBFAM: 11;

          hence thesis by Th10;

        end;

      end;

    end

    theorem :: CLOSURE1:12

    ( id ( bool A)) is reflexive MSSetOp of A

    proof

      reconsider a = ( id ( bool A)) as MSSetOp of A;

      a is reflexive by Th8;

      hence thesis;

    end;

    theorem :: CLOSURE1:13

    ( id ( bool A)) is monotonic MSSetOp of A

    proof

      reconsider a = ( id ( bool A)) as MSSetOp of A;

      a is monotonic by Th9;

      hence thesis;

    end;

    theorem :: CLOSURE1:14

    ( id ( bool A)) is idempotent MSSetOp of A

    proof

      reconsider a = ( id ( bool A)) as MSSetOp of A;

      a is idempotent by Th8;

      hence thesis;

    end;

    theorem :: CLOSURE1:15

    ( id ( bool A)) is topological MSSetOp of A

    proof

      reconsider a = ( id ( bool A)) as MSSetOp of A;

      a is topological

      proof

        let X,Y be Element of ( bool A);

        Y in ( bool A) by MSSUBFAM: 12;

        then

         A1: Y c= A by MBOOLEAN: 1;

        X in ( bool A) by MSSUBFAM: 12;

        then X c= A by MBOOLEAN: 1;

        then (X (\/) Y) c= A by A1, PBOOLE: 16;

        then (X (\/) Y) in ( bool A) by MBOOLEAN: 1;

        then (X (\/) Y) is Element of ( bool A) by MSSUBFAM: 11;

        hence thesis by Th10;

      end;

      hence thesis;

    end;

    reserve P,R for MSSetOp of M,

E,T for Element of ( bool M);

    theorem :: CLOSURE1:16

    E = M & P is reflexive implies E = (P .. E)

    proof

      assume

       A1: E = M;

      assume P is reflexive;

      then

       A2: E c= (P .. E);

      (P .. E) in ( bool E) by A1, MSSUBFAM: 12;

      then (P .. E) c= E by MBOOLEAN: 18;

      hence thesis by A2, PBOOLE: 146;

    end;

    theorem :: CLOSURE1:17

    (P is reflexive & for X be Element of ( bool M) holds (P .. X) c= X) implies P is idempotent

    proof

      assume that

       A1: P is reflexive and

       A2: for X be Element of ( bool M) holds (P .. X) c= X;

      let X be Element of ( bool M);

      

       A3: (P .. X) c= (P .. (P .. X)) by A1;

      (P .. (P .. X)) c= (P .. X) by A2;

      hence thesis by A3, PBOOLE: 146;

    end;

    theorem :: CLOSURE1:18

    P is monotonic implies (P .. (E (/\) T)) c= ((P .. E) (/\) (P .. T))

    proof

      assume

       A1: P is monotonic;

      E in ( bool M) by MSSUBFAM: 12;

      then E c= M by MBOOLEAN: 1;

      then (E (/\) T) c= M by MBOOLEAN: 14;

      then (E (/\) T) in ( bool M) by MBOOLEAN: 1;

      then

       A2: (E (/\) T) is Element of ( bool M) by MSSUBFAM: 11;

      (E (/\) T) c= T by PBOOLE: 15;

      then

       A3: (P .. (E (/\) T)) c= (P .. T) by A1, A2;

      (E (/\) T) c= E by PBOOLE: 15;

      then (P .. (E (/\) T)) c= (P .. E) by A1, A2;

      hence thesis by A3, PBOOLE: 17;

    end;

    registration

      let I, M;

      cluster topological -> monotonic for MSSetOp of M;

      coherence

      proof

        let P be MSSetOp of M such that

         A1: P is topological;

        let X,Y be Element of ( bool M) such that

         A2: X c= Y;

        ((P .. X) (\/) (P .. Y)) = (P .. (X (\/) Y)) by A1

        .= (P .. Y) by A2, PBOOLE: 22;

        hence thesis by PBOOLE: 26;

      end;

    end

    theorem :: CLOSURE1:19

    P is topological implies ((P .. E) (\) (P .. T)) c= (P .. (E (\) T))

    proof

      E in ( bool M) by MSSUBFAM: 12;

      then E c= M by MBOOLEAN: 1;

      then (E (\) T) c= M by MBOOLEAN: 15;

      then (E (\) T) in ( bool M) by MBOOLEAN: 1;

      then

       A1: (E (\) T) is Element of ( bool M) by MSSUBFAM: 11;

      assume

       A2: P is topological;

      

      then ((P .. E) (\/) (P .. T)) = (P .. (E (\/) T))

      .= (P .. ((E (\) T) (\/) T)) by PBOOLE: 67

      .= ((P .. (E (\) T)) (\/) (P .. T)) by A1, A2;

      then (P .. E) c= ((P .. (E (\) T)) (\/) (P .. T)) by PBOOLE: 14;

      then ((P .. E) (\) (P .. T)) c= (((P .. (E (\) T)) (\/) (P .. T)) (\) (P .. T)) by PBOOLE: 53;

      then

       A3: ((P .. E) (\) (P .. T)) c= ((P .. (E (\) T)) (\) (P .. T)) by PBOOLE: 75;

      ((P .. (E (\) T)) (\) (P .. T)) c= (P .. (E (\) T)) by PBOOLE: 56;

      hence thesis by A3, PBOOLE: 13;

    end;

    definition

      let I, M, R, P;

      :: original: **

      redefine

      func P ** R -> MSSetOp of M ;

      coherence

      proof

        (P ** R) is ManySortedFunction of ( bool M), ( bool M);

        hence thesis;

      end;

    end

    theorem :: CLOSURE1:20

    P is reflexive & R is reflexive implies (P ** R) is reflexive

    proof

      assume

       A1: P is reflexive & R is reflexive;

      let X be Element of ( bool M);

      X c= (R .. X) & (R .. X) c= (P .. (R .. X)) by A1;

      then ( doms R) = ( bool M) & X c= (P .. (R .. X)) by MSSUBFAM: 17, PBOOLE: 13;

      hence thesis by Th4, MSSUBFAM: 12;

    end;

    theorem :: CLOSURE1:21

    P is monotonic & R is monotonic implies (P ** R) is monotonic

    proof

      assume that

       A1: P is monotonic and

       A2: R is monotonic;

      

       A3: ( doms R) = ( bool M) by MSSUBFAM: 17;

      let X,Y be Element of ( bool M);

      assume X c= Y;

      then (R .. X) c= (R .. Y) by A2;

      then (P .. (R .. X)) c= (P .. (R .. Y)) by A1;

      then (P .. (R .. X)) c= ((P ** R) .. Y) by A3, Th4, MSSUBFAM: 12;

      hence thesis by A3, Th4, MSSUBFAM: 12;

    end;

    theorem :: CLOSURE1:22

    P is idempotent & R is idempotent & (P ** R) = (R ** P) implies (P ** R) is idempotent

    proof

      assume that

       A1: P is idempotent and

       A2: R is idempotent and

       A3: (P ** R) = (R ** P);

      let X be Element of ( bool M);

      

       A4: ( doms P) = ( bool M) by MSSUBFAM: 17;

      

       A5: ( doms R) = ( bool M) by MSSUBFAM: 17;

      

      hence ((P ** R) .. X) = (P .. (R .. X)) by Th4, MSSUBFAM: 12

      .= (P .. (R .. (R .. X))) by A2

      .= (P .. (P .. (R .. (R .. X)))) by A1

      .= (P .. ((R ** P) .. (R .. X))) by A3, A5, Th4, MSSUBFAM: 12

      .= (P .. (R .. (P .. (R .. X)))) by A4, Th4, MSSUBFAM: 12

      .= (P .. (R .. ((P ** R) .. X))) by A5, Th4, MSSUBFAM: 12

      .= ((P ** R) .. ((P ** R) .. X)) by A5, Th4, MSSUBFAM: 12;

    end;

    theorem :: CLOSURE1:23

    P is topological & R is topological implies (P ** R) is topological

    proof

      assume that

       A1: P is topological and

       A2: R is topological;

      let X,Y be Element of ( bool M);

      

       A3: ( doms R) = ( bool M) by MSSUBFAM: 17;

      Y in ( bool M) by MSSUBFAM: 12;

      then

       A4: Y c= M by MBOOLEAN: 1;

      X in ( bool M) by MSSUBFAM: 12;

      then X c= M by MBOOLEAN: 1;

      then (X (\/) Y) c= M by A4, PBOOLE: 16;

      then (X (\/) Y) in ( doms R) by A3, MBOOLEAN: 1;

      

      hence ((P ** R) .. (X (\/) Y)) = (P .. (R .. (X (\/) Y))) by Th4

      .= (P .. ((R .. X) (\/) (R .. Y))) by A2

      .= ((P .. (R .. X)) (\/) (P .. (R .. Y))) by A1

      .= (((P ** R) .. X) (\/) (P .. (R .. Y))) by A3, Th4, MSSUBFAM: 12

      .= (((P ** R) .. X) (\/) ((P ** R) .. Y)) by A3, Th4, MSSUBFAM: 12;

    end;

     Lm2:

    now

      let I, M, i;

      let a be ManySortedSet of I, b be Element of ( bool (M . i)) such that

       A1: a = (( EmptyMS I) +* (i .--> b));

      

       A2: ( dom (i .--> b)) = {i};

      ( EmptyMS I) c= M by MBOOLEAN: 5;

      then

       A3: ( EmptyMS I) in ( bool M) by MBOOLEAN: 1;

      thus a in ( bool M)

      proof

        let j be object such that

         A4: j in I;

        i in {i} by TARSKI:def 1;

        

        then

         A5: (a . i) = ((i .--> b) . i) by A1, A2, FUNCT_4: 13

        .= b by FUNCOP_1: 72;

        now

          per cases ;

            case

             A6: j = i;

            then b in ( bool (M . j));

            hence thesis by A4, A5, A6, MBOOLEAN:def 1;

          end;

            case j <> i;

            then not j in ( dom (i .--> b)) by TARSKI:def 1;

            then (a . j) = (( EmptyMS I) . j) by A1, FUNCT_4: 11;

            hence thesis by A3, A4;

          end;

        end;

        hence thesis;

      end;

    end;

    theorem :: CLOSURE1:24

    

     Th24: P is reflexive & i in I & f = (P . i) implies for x be Element of ( bool (M . i)) holds x c= (f . x)

    proof

      assume that

       A1: P is reflexive and

       A2: i in I and

       A3: f = (P . i);

      let x be Element of ( bool (M . i));

      ( dom (( EmptyMS I) +* (i .--> x))) = I by A2, PZFMISC1: 1;

      then

      reconsider X = (( EmptyMS I) +* (i .--> x)) as ManySortedSet of I by PARTFUN1:def 2, RELAT_1:def 18;

      X is Element of ( bool M) by Lm2, MSSUBFAM: 11;

      then X c= (P .. X) by A1;

      then

       A4: (X . i) c= ((P .. X) . i) by A2;

      ( dom (i .--> x)) = {i} & i in {i} by TARSKI:def 1;

      

      then

       A5: (X . i) = ((i .--> x) . i) by FUNCT_4: 13

      .= x by FUNCOP_1: 72;

      i in ( dom X) & i in ( dom P) by A2, PARTFUN1:def 2;

      then i in (( dom P) /\ ( dom X)) by XBOOLE_0:def 4;

      then i in ( dom (P .. X)) by PRALG_1:def 19;

      hence thesis by A3, A5, A4, PRALG_1:def 19;

    end;

    theorem :: CLOSURE1:25

    

     Th25: P is monotonic & i in I & f = (P . i) implies for x,y be Element of ( bool (M . i)) st x c= y holds (f . x) c= (f . y)

    proof

      assume that

       A1: P is monotonic and

       A2: i in I and

       A3: f = (P . i);

      let x,y be Element of ( bool (M . i)) such that

       A4: x c= y;

      ( dom (( EmptyMS I) +* (i .--> y))) = I by A2, PZFMISC1: 1;

      then

      reconsider Y = (( EmptyMS I) +* (i .--> y)) as ManySortedSet of I by PARTFUN1:def 2, RELAT_1:def 18;

      ( dom (( EmptyMS I) +* (i .--> x))) = I by A2, PZFMISC1: 1;

      then

      reconsider X = (( EmptyMS I) +* (i .--> x)) as ManySortedSet of I by PARTFUN1:def 2, RELAT_1:def 18;

      

       A5: i in {i} by TARSKI:def 1;

      ( dom (i .--> y)) = {i};

      

      then

       A6: (Y . i) = ((i .--> y) . i) by A5, FUNCT_4: 13

      .= y by FUNCOP_1: 72;

      ( dom (i .--> x)) = {i};

      

      then

       A8: (X . i) = ((i .--> x) . i) by A5, FUNCT_4: 13

      .= x by FUNCOP_1: 72;

      

       A9: X c= Y

      proof

        let s be object such that s in I;

        per cases ;

          suppose s = i;

          hence thesis by A4, A8, A6;

        end;

          suppose s <> i;

          then not s in ( dom (i .--> x)) by TARSKI:def 1;

          then

           A10: (X . s) = (( EmptyMS I) . s) by FUNCT_4: 11;

          thus thesis by A10;

        end;

      end;

      

       A11: i in ( dom P) by A2, PARTFUN1:def 2;

      X is Element of ( bool M) & Y is Element of ( bool M) by Lm2, MSSUBFAM: 11;

      then (P .. X) c= (P .. Y) by A1, A9;

      then

       A12: ((P .. X) . i) c= ((P .. Y) . i) by A2;

      i in ( dom Y) by A2, PARTFUN1:def 2;

      then i in (( dom P) /\ ( dom Y)) by A11, XBOOLE_0:def 4;

      then i in ( dom (P .. Y)) by PRALG_1:def 19;

      then

       W: ((P .. Y) . i) = (f . (Y . i)) by PRALG_1:def 19, A3;

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

      then i in ( dom X) by A2;

      then i in (( dom P) /\ ( dom X)) by A11, XBOOLE_0:def 4;

      then i in ( dom (P .. X)) by PRALG_1:def 19;

      then (f . (X . i)) = ((P .. X) . i) by A3, PRALG_1:def 19;

      then (f . (X . i)) c= ((P .. Y) . i) by A12;

      hence thesis by A8, A6, W;

    end;

    theorem :: CLOSURE1:26

    

     Th26: P is idempotent & i in I & f = (P . i) implies for x be Element of ( bool (M . i)) holds (f . x) = (f . (f . x))

    proof

      assume that

       A1: P is idempotent and

       A2: i in I and

       A3: f = (P . i);

      

       A4: i in ( dom P) by A2, PARTFUN1:def 2;

      let x be Element of ( bool (M . i));

      ( dom (( EmptyMS I) +* (i .--> x))) = I by A2, PZFMISC1: 1;

      then

      reconsider X = (( EmptyMS I) +* (i .--> x)) as ManySortedSet of I by PARTFUN1:def 2, RELAT_1:def 18;

      

       A5: X is Element of ( bool M) by Lm2, MSSUBFAM: 11;

      ( dom (i .--> x)) = {i} & i in {i} by TARSKI:def 1;

      

      then

       A6: (X . i) = ((i .--> x) . i) by FUNCT_4: 13

      .= x by FUNCOP_1: 72;

      i in ( dom X) by A2, PARTFUN1:def 2;

      then i in (( dom P) /\ ( dom X)) by A4, XBOOLE_0:def 4;

      then

       A7: i in ( dom (P .. X)) by PRALG_1:def 19;

      i in ( dom P) by A2, PARTFUN1:def 2;

      then i in (( dom P) /\ ( dom (P .. X))) by A7, XBOOLE_0:def 4;

      then

       B1: i in ( dom (P .. (P .. X))) by PRALG_1:def 19;

      

      thus (f . x) = ((P .. X) . i) by A6, A3, PRALG_1:def 19, A7

      .= ((P .. (P .. X)) . i) by A1, A5

      .= (f . ((P .. X) . i)) by B1, A3, PRALG_1:def 19

      .= (f . (f . x)) by A3, A6, A7, PRALG_1:def 19;

    end;

    theorem :: CLOSURE1:27

    P is topological & i in I & f = (P . i) implies for x,y be Element of ( bool (M . i)) holds (f . (x \/ y)) = ((f . x) \/ (f . y))

    proof

      assume that

       A1: P is topological and

       A2: i in I and

       A3: f = (P . i);

      

       A4: i in ( dom P) by A2, PARTFUN1:def 2;

      let x,y be Element of ( bool (M . i));

      ( dom (( EmptyMS I) +* (i .--> y))) = I by A2, PZFMISC1: 1;

      then

      reconsider Y = (( EmptyMS I) +* (i .--> y)) as ManySortedSet of I by PARTFUN1:def 2, RELAT_1:def 18;

      ( dom (( EmptyMS I) +* (i .--> x))) = I by A2, PZFMISC1: 1;

      then

      reconsider X = (( EmptyMS I) +* (i .--> x)) as ManySortedSet of I by PARTFUN1:def 2, RELAT_1:def 18;

      

       A5: i in {i} by TARSKI:def 1;

      ( dom (i .--> y)) = {i};

      

      then

       A6: (Y . i) = ((i .--> y) . i) by A5, FUNCT_4: 13

      .= y by FUNCOP_1: 72;

      

       A7: X is Element of ( bool M) & Y is Element of ( bool M) by Lm2, MSSUBFAM: 11;

      i in ( dom (X (\/) Y)) by A2, PARTFUN1:def 2;

      then i in (( dom P) /\ ( dom (X (\/) Y))) by A4, XBOOLE_0:def 4;

      then

       B1: i in ( dom (P .. (X (\/) Y))) by PRALG_1:def 19;

      i in ( dom X) by A2, PARTFUN1:def 2;

      then i in (( dom P) /\ ( dom X)) by XBOOLE_0:def 4, A4;

      then

       B2: i in ( dom (P .. X)) by PRALG_1:def 19;

      i in ( dom Y) by A2, PARTFUN1:def 2;

      then i in (( dom P) /\ ( dom Y)) by XBOOLE_0:def 4, A4;

      then

       B3: i in ( dom (P .. Y)) by PRALG_1:def 19;

      ( dom (i .--> x)) = {i};

      

      then

       A8: (X . i) = ((i .--> x) . i) by A5, FUNCT_4: 13

      .= x by FUNCOP_1: 72;

      

      hence (f . (x \/ y)) = (f . ((X (\/) Y) . i)) by A2, A6, PBOOLE:def 4

      .= ((P .. (X (\/) Y)) . i) by A3, PRALG_1:def 19, B1

      .= (((P .. X) (\/) (P .. Y)) . i) by A1, A7

      .= (((P .. X) . i) \/ ((P .. Y) . i)) by A2, PBOOLE:def 4

      .= ((f . (X . i)) \/ ((P .. Y) . i)) by A3, PRALG_1:def 19, B2

      .= ((f . x) \/ (f . y)) by A3, A8, A6, PRALG_1:def 19, B3;

    end;

    begin

    reserve S for 1-sorted;

    definition

      let S;

      struct ( many-sorted over S) MSClosureStr over S (# the Sorts -> ManySortedSet of the carrier of S,

the Family -> MSSubsetFamily of the Sorts #)

       attr strict strict;

    end

    reserve MS for many-sorted over S;

    definition

      let S;

      let IT be MSClosureStr over S;

      :: CLOSURE1:def5

      attr IT is additive means

      : Def5: the Family of IT is additive;

      :: CLOSURE1:def6

      attr IT is absolutely-additive means

      : Def6: the Family of IT is absolutely-additive;

      :: CLOSURE1:def7

      attr IT is multiplicative means

      : Def7: the Family of IT is multiplicative;

      :: CLOSURE1:def8

      attr IT is absolutely-multiplicative means

      : Def8: the Family of IT is absolutely-multiplicative;

      :: CLOSURE1:def9

      attr IT is properly-upper-bound means

      : Def9: the Family of IT is properly-upper-bound;

      :: CLOSURE1:def10

      attr IT is properly-lower-bound means

      : Def10: the Family of IT is properly-lower-bound;

    end

    definition

      let S, MS;

      :: CLOSURE1:def11

      func MSFull MS -> MSClosureStr over S equals MSClosureStr (# the Sorts of MS, ( bool the Sorts of MS) #);

      correctness ;

    end

    registration

      let S, MS;

      cluster ( MSFull MS) -> strict additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound;

      coherence ;

    end

    registration

      let S;

      let MS be non-empty many-sorted over S;

      cluster ( MSFull MS) -> non-empty;

      coherence ;

    end

    registration

      let S;

      cluster strict non-empty additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound for MSClosureStr over S;

      existence

      proof

        set a = the non-empty many-sorted over S;

        take ( MSFull a);

        thus thesis;

      end;

    end

    registration

      let S;

      let CS be additive MSClosureStr over S;

      cluster the Family of CS -> additive;

      coherence by Def5;

    end

    registration

      let S;

      let CS be absolutely-additive MSClosureStr over S;

      cluster the Family of CS -> absolutely-additive;

      coherence by Def6;

    end

    registration

      let S;

      let CS be multiplicative MSClosureStr over S;

      cluster the Family of CS -> multiplicative;

      coherence by Def7;

    end

    registration

      let S;

      let CS be absolutely-multiplicative MSClosureStr over S;

      cluster the Family of CS -> absolutely-multiplicative;

      coherence by Def8;

    end

    registration

      let S;

      let CS be properly-upper-bound MSClosureStr over S;

      cluster the Family of CS -> properly-upper-bound;

      coherence by Def9;

    end

    registration

      let S;

      let CS be properly-lower-bound MSClosureStr over S;

      cluster the Family of CS -> properly-lower-bound;

      coherence by Def10;

    end

    registration

      let S;

      let M be non-empty ManySortedSet of the carrier of S;

      let F be MSSubsetFamily of M;

      cluster MSClosureStr (# M, F #) -> non-empty;

      coherence ;

    end

    registration

      let S, MS;

      let F be additive MSSubsetFamily of the Sorts of MS;

      cluster MSClosureStr (# the Sorts of MS, F #) -> additive;

      coherence ;

    end

    registration

      let S, MS;

      let F be absolutely-additive MSSubsetFamily of the Sorts of MS;

      cluster MSClosureStr (# the Sorts of MS, F #) -> absolutely-additive;

      coherence ;

    end

    registration

      let S, MS;

      let F be multiplicative MSSubsetFamily of the Sorts of MS;

      cluster MSClosureStr (# the Sorts of MS, F #) -> multiplicative;

      coherence ;

    end

    registration

      let S, MS;

      let F be absolutely-multiplicative MSSubsetFamily of the Sorts of MS;

      cluster MSClosureStr (# the Sorts of MS, F #) -> absolutely-multiplicative;

      coherence ;

    end

    registration

      let S, MS;

      let F be properly-upper-bound MSSubsetFamily of the Sorts of MS;

      cluster MSClosureStr (# the Sorts of MS, F #) -> properly-upper-bound;

      coherence ;

    end

    registration

      let S, MS;

      let F be properly-lower-bound MSSubsetFamily of the Sorts of MS;

      cluster MSClosureStr (# the Sorts of MS, F #) -> properly-lower-bound;

      coherence ;

    end

    registration

      let S;

      cluster absolutely-additive -> additive for MSClosureStr over S;

      coherence ;

    end

    registration

      let S;

      cluster absolutely-multiplicative -> multiplicative for MSClosureStr over S;

      coherence ;

    end

    registration

      let S;

      cluster absolutely-multiplicative -> properly-upper-bound for MSClosureStr over S;

      coherence ;

    end

    registration

      let S;

      cluster absolutely-additive -> properly-lower-bound for MSClosureStr over S;

      coherence ;

    end

    definition

      let S;

      mode MSClosureSystem of S is absolutely-multiplicative MSClosureStr over S;

    end

    definition

      let I, M;

      mode MSClosureOperator of M is reflexive monotonic idempotent MSSetOp of M;

    end

    definition

      let I, M;

      let F be ManySortedFunction of M, M;

      :: CLOSURE1:def12

      func MSFixPoints F -> ManySortedSubset of M means

      : Def12: for i be object st i in I holds x in (it . i) iff ex f be Function st f = (F . i) & x in ( dom f) & (f . x) = x;

      existence

      proof

        defpred P[ object, object] means ex D2 be set st D2 = $2 & for x be object holds x in D2 iff x in (M . $1) & ex f be Function st f = (F . $1) & x in ( dom f) & (f . x) = x;

         A1:

        now

          let i be object such that i in I;

          defpred R[ object] means ex f be Function st f = (F . i) & $1 in ( dom f) & (f . $1) = $1;

          consider j be set such that

           A2: for x be object holds x in j iff x in (M . i) & R[x] from XBOOLE_0:sch 1;

          reconsider j as object;

          take j;

          thus P[i, j] by A2;

        end;

        consider A be ManySortedSet of I such that

         A3: for i be object st i in I holds P[i, (A . i)] from PBOOLE:sch 3( A1);

        A is ManySortedSubset of M

        proof

          let i be object such that

           A4: i in I;

          let x be object;

          assume

           A5: x in (A . i);

           P[i, (A . i)] by A3, A4;

          hence thesis by A5;

        end;

        then

        reconsider A as ManySortedSubset of M;

        take A;

        thus for i be object st i in I holds x in (A . i) iff ex f be Function st f = (F . i) & x in ( dom f) & (f . x) = x

        proof

          let i be object;

          assume

           A6: i in I;

          then P[i, (A . i)] by A3;

          hence x in (A . i) implies ex f be Function st f = (F . i) & x in ( dom f) & (f . x) = x;

          given f be Function such that

           A7: f = (F . i) and

           A8: x in ( dom f) & (f . x) = x;

          ( doms F) = M by MSSUBFAM: 17;

          then

           A9: ( dom f) = (M . i) by A6, A7, MSSUBFAM: 14;

           P[i, (A . i)] by A3, A6;

          hence thesis by A7, A8, A9;

        end;

      end;

      uniqueness

      proof

        let A,B be ManySortedSubset of M such that

         A10: for i be object st i in I holds x in (A . i) iff ex f be Function st f = (F . i) & x in ( dom f) & (f . x) = x and

         A11: for i be object st i in I holds x in (B . i) iff ex f be Function st f = (F . i) & x in ( dom f) & (f . x) = x;

        now

          let i be object such that

           A12: i in I;

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

          proof

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

            proof

              let x be object;

              assume x in (A . i);

              then ex f be Function st f = (F . i) & x in ( dom f) & (f . x) = x by A10, A12;

              hence thesis by A11, A12;

            end;

            let x be object;

            assume x in (B . i);

            then ex f be Function st f = (F . i) & x in ( dom f) & (f . x) = x by A11, A12;

            hence thesis by A10, A12;

          end;

        end;

        hence A = B;

      end;

    end

    registration

      let I;

      let M be empty-yielding ManySortedSet of I;

      let F be ManySortedFunction of M, M;

      cluster ( MSFixPoints F) -> empty-yielding;

      coherence

      proof

        let i be object such that

         A1: i in I;

        assume (( MSFixPoints F) . i) is non empty;

        then

        consider x be object such that

         A2: x in (( MSFixPoints F) . i);

        consider f be Function such that

         A3: f = (F . i) and

         A4: x in ( dom f) and (f . x) = x by A1, A2, Def12;

        (M . i) = {} ;

        then f is Function of {} , {} by A1, A3, PBOOLE:def 15;

        hence contradiction by A4;

      end;

    end

    theorem :: CLOSURE1:28

    

     Th28: for F be ManySortedFunction of M, M holds A in M & (F .. A) = A iff A in ( MSFixPoints F)

    proof

      let F be ManySortedFunction of M, M;

      thus A in M & (F .. A) = A implies A in ( MSFixPoints F)

      proof

        assume that

         A1: A in M and

         A2: (F .. A) = A;

        let i be object;

        assume

         A3: i in I;

        then

        reconsider f = (F . i) as Function of (M . i), (M . i) by PBOOLE:def 15;

        i in ( dom (F .. A)) by A3, PARTFUN1:def 2;

        then

         A4: (f . (A . i)) = (A . i) by A2, PRALG_1:def 19;

        M = ( doms F) by MSSUBFAM: 17;

        then (M . i) = ( dom f) by A3, MSSUBFAM: 14;

        then (A . i) in ( dom f) by A1, A3;

        hence thesis by A3, A4, Def12;

      end;

      assume

       A5: A in ( MSFixPoints F);

      thus A in M

      proof

        let i be object;

        

         A6: M = ( doms F) by MSSUBFAM: 17;

        assume

         A7: i in I;

        then (A . i) in (( MSFixPoints F) . i) by A5;

        then ex f be Function st f = (F . i) & (A . i) in ( dom f) & (f . (A . i)) = (A . i) by A7, Def12;

        hence thesis by A7, A6, MSSUBFAM: 14;

      end;

      now

        let i be object;

        assume

         A8: i in I;

        then (A . i) in (( MSFixPoints F) . i) by A5;

        then

         A9: ex f be Function st f = (F . i) & (A . i) in ( dom f) & (f . (A . i)) = (A . i) by A8, Def12;

        i in ( dom A) & i in ( dom F) by A8, PARTFUN1:def 2;

        then i in (( dom F) /\ ( dom A)) by XBOOLE_0:def 4;

        then i in ( dom (F .. A)) by PRALG_1:def 19;

        hence ((F .. A) . i) = (A . i) by A9, PRALG_1:def 19;

      end;

      hence thesis;

    end;

    theorem :: CLOSURE1:29

    ( MSFixPoints ( id A)) = A

    proof

      now

        let i be object such that

         A1: i in I;

        thus (( MSFixPoints ( id A)) . i) = (A . i)

        proof

          thus (( MSFixPoints ( id A)) . i) c= (A . i)

          proof

            let x be object;

            assume x in (( MSFixPoints ( id A)) . i);

            then

            consider f be Function such that

             A2: f = (( id A) . i) and

             A3: x in ( dom f) and (f . x) = x by A1, Def12;

            f is Function of (A . i), (A . i) by A1, A2, PBOOLE:def 15;

            hence thesis by A3, FUNCT_2: 52;

          end;

          reconsider f = (( id A) . i) as Function of (A . i), (A . i) by A1, PBOOLE:def 15;

          let x be object such that

           A4: x in (A . i);

          

           A5: x in ( dom f) by A4, FUNCT_2: 52;

          f = ( id (A . i)) by A1, MSUALG_3:def 1;

          then (f . x) = x by A4, FUNCT_1: 18;

          hence thesis by A1, A5, Def12;

        end;

      end;

      hence thesis;

    end;

    theorem :: CLOSURE1:30

    

     Th30: for A be ManySortedSet of the carrier of S holds for J be reflexive monotonic MSSetOp of A holds for D be MSSubsetFamily of A st D = ( MSFixPoints J) holds MSClosureStr (# A, D #) is MSClosureSystem of S

    proof

      let A be ManySortedSet of the carrier of S, J be reflexive monotonic MSSetOp of A, D be MSSubsetFamily of A such that

       A1: D = ( MSFixPoints J);

      D is absolutely-multiplicative

      proof

        let F be MSSubsetFamily of A such that

         A2: F c= D;

        

         A3: (J .. ( meet F)) c= ( meet F)

        proof

          let i be object;

          assume

           A4: i in the carrier of S;

          then

          reconsider j = (J . i) as Function of (( bool A) . i), (( bool A) . i) by PBOOLE:def 15;

          

           A5: i in ( dom J) by A4, PARTFUN1:def 2;

          i in ( dom ( meet F)) by A4, PARTFUN1:def 2;

          then i in (( dom J) /\ ( dom ( meet F))) by A5, XBOOLE_0:def 4;

          then

           a5: i in ( dom (J .. ( meet F))) by PRALG_1:def 19;

          consider Q be Subset-Family of (A . i) such that

           A6: Q = (F . i) and

           A7: (( meet F) . i) = ( Intersect Q) by A4, MSSUBFAM:def 1;

           A8:

          now

            let x such that

             A9: x in Q;

            Q c= (D . i) by A2, A4, A6;

            then ex jj be Function st jj = (J . i) & x in ( dom jj) & (jj . x) = x by A1, A4, A9, Def12;

            hence (j . ( Intersect Q)) c= x by A4, A9, Th25, MSSUBFAM: 2;

          end;

          (( bool A) . i) = ( bool (A . i)) by A4, MBOOLEAN:def 1;

          then (j . ( Intersect Q)) in ( bool (A . i)) by FUNCT_2: 5;

          then (j . ( Intersect Q)) c= ( Intersect Q) by A8, MSSUBFAM: 4;

          hence thesis by A7, PRALG_1:def 19, a5;

        end;

        ( meet F) c= A by PBOOLE:def 18;

        then

         A10: ( meet F) in ( bool A) by MBOOLEAN: 18;

        then ( meet F) is Element of ( bool A) by MSSUBFAM: 11;

        then ( meet F) c= (J .. ( meet F)) by Def1;

        then (J .. ( meet F)) = ( meet F) by A3, PBOOLE: 146;

        hence thesis by A1, A10, Th28;

      end;

      hence thesis;

    end;

    theorem :: CLOSURE1:31

    

     Th31: for D be properly-upper-bound MSSubsetFamily of M holds for X be Element of ( bool M) holds ex SF be non-empty MSSubsetFamily of M st for Y be ManySortedSet of I holds Y in SF iff Y in D & X c= Y

    proof

      let D be properly-upper-bound MSSubsetFamily of M, X be Element of ( bool M);

      defpred P[ object, object] means ex D2 be set st D2 = $2 & (X . $1) c= D2;

      consider SF be ManySortedSet of I such that

       A1: for i be object st i in I holds for e be object holds e in (SF . i) iff e in (D . i) & P[i, e] from PBOOLE:sch 2;

      

       A2: D c= ( bool M) by PBOOLE:def 18;

      SF is ManySortedSubset of ( bool M)

      proof

        let i be object;

        assume

         A3: i in I;

        then (D . i) c= (( bool M) . i) by A2;

        then

         A4: (D . i) c= ( bool (M . i)) by A3, MBOOLEAN:def 1;

        (SF . i) c= ( bool (M . i))

        proof

          let x be object;

          assume x in (SF . i);

          then x in (D . i) by A1, A3;

          hence thesis by A4;

        end;

        hence (SF . i) c= (( bool M) . i) by A3, MBOOLEAN:def 1;

      end;

      then

      reconsider SF as ManySortedSubset of ( bool M);

      reconsider SF as MSSubsetFamily of M;

      SF is non-empty

      proof

        let i be object such that

         A5: i in I;

        M in D by MSSUBFAM:def 6;

        then

         A6: (M . i) in (D . i) by A5;

        X in ( bool M) by MSSUBFAM: 12;

        then X c= M by MBOOLEAN: 18;

        then (X . i) c= (M . i) by A5;

        hence thesis by A1, A5, A6;

      end;

      then

      reconsider SF as non-empty MSSubsetFamily of M;

      take SF;

      let Y be ManySortedSet of I;

      thus Y in SF implies Y in D & X c= Y

      proof

        assume

         A7: Y in SF;

        thus Y in D

        proof

          let i be object;

          assume

           A8: i in I;

          then (Y . i) in (SF . i) by A7;

          hence thesis by A1, A8;

        end;

        thus X c= Y

        proof

          let i be object;

          assume

           A9: i in I;

          then (Y . i) in (SF . i) by A7;

          then (Y . i) in (D . i) & P[i, (Y . i)] by A1, A9;

          hence thesis;

        end;

      end;

      assume

       A10: Y in D & X c= Y;

      let i be object;

      assume

       A11: i in I;

      then (Y . i) in (D . i) & (X . i) c= (Y . i) by A10;

      hence thesis by A1, A11;

    end;

    theorem :: CLOSURE1:32

    

     Th32: for D be properly-upper-bound MSSubsetFamily of M holds for X be Element of ( bool M) holds for SF be non-empty MSSubsetFamily of M st (for Y be ManySortedSet of I holds Y in SF iff Y in D & X c= Y) holds for i be set, Di be non empty set st i in I & Di = (D . i) holds (SF . i) = { z where z be Element of Di : (X . i) c= z }

    proof

      let D be properly-upper-bound MSSubsetFamily of M, X be Element of ( bool M), SF be non-empty MSSubsetFamily of M such that

       A1: for Y be ManySortedSet of I holds Y in SF iff Y in D & X c= Y;

      let i be set, Di be non empty set such that

       A2: i in I and

       A3: Di = (D . i);

      thus (SF . i) c= { z where z be Element of Di : (X . i) c= z }

      proof

        consider K be ManySortedSet of I such that

         A4: K in SF by PBOOLE: 134;

        let x be object such that

         A5: x in (SF . i);

        ( dom (K +* (i .--> x))) = I by A2, PZFMISC1: 1;

        then

        reconsider L = (K +* (i .--> x)) as ManySortedSet of I by PARTFUN1:def 2, RELAT_1:def 18;

        

         A6: ( dom (i .--> x)) = {i};

        i in {i} by TARSKI:def 1;

        

        then

         A7: (L . i) = ((i .--> x) . i) by A6, FUNCT_4: 13

        .= x by FUNCOP_1: 72;

        

         A8: L in SF

        proof

          let s be object such that

           A9: s in I;

          per cases ;

            suppose s = i;

            hence thesis by A5, A7;

          end;

            suppose s <> i;

            then not s in ( dom (i .--> x)) by TARSKI:def 1;

            then (L . s) = (K . s) by FUNCT_4: 11;

            hence thesis by A4, A9;

          end;

        end;

        then X c= L by A1;

        then

         A10: (X . i) c= (L . i) by A2;

        L in D by A1, A8;

        then (L . i) in (D . i) by A2;

        hence thesis by A3, A7, A10;

      end;

      let x be object;

      assume x in { z where z be Element of Di : (X . i) c= z };

      then

      consider g be Element of Di such that

       A11: g = x and

       A12: (X . i) c= g;

      ( dom (M +* (i .--> g))) = I by A2, PZFMISC1: 1;

      then

      reconsider L1 = (M +* (i .--> g)) as ManySortedSet of I by PARTFUN1:def 2, RELAT_1:def 18;

      

       A13: ( dom (i .--> g)) = {i};

      i in {i} by TARSKI:def 1;

      

      then

       A14: (L1 . i) = ((i .--> g) . i) by A13, FUNCT_4: 13

      .= g by FUNCOP_1: 72;

      

       A15: X c= L1

      proof

        let s be object such that

         A16: s in I;

        per cases ;

          suppose s = i;

          hence thesis by A12, A14;

        end;

          suppose

           A17: s <> i;

          X in ( bool M) by MSSUBFAM: 12;

          then

           A18: X c= M by MBOOLEAN: 18;

           not s in ( dom (i .--> g)) by A17, TARSKI:def 1;

          then (L1 . s) = (M . s) by FUNCT_4: 11;

          hence thesis by A16, A18;

        end;

      end;

      

       A19: M in D by MSSUBFAM:def 6;

      L1 in D

      proof

        let s be object such that

         A20: s in I;

        per cases ;

          suppose s = i;

          hence thesis by A3, A14;

        end;

          suppose s <> i;

          then not s in ( dom (i .--> g)) by TARSKI:def 1;

          then (L1 . s) = (M . s) by FUNCT_4: 11;

          hence thesis by A19, A20;

        end;

      end;

      then L1 in SF by A1, A15;

      hence thesis by A2, A11, A14;

    end;

    theorem :: CLOSURE1:33

    

     Th33: for D be properly-upper-bound MSSubsetFamily of M holds ex J be MSSetOp of M st for X be Element of ( bool M) holds for SF be non-empty MSSubsetFamily of M st (for Y be ManySortedSet of I holds Y in SF iff Y in D & X c= Y) holds (J .. X) = ( meet SF)

    proof

      let D be properly-upper-bound MSSubsetFamily of M;

      set G = ( bool M);

      defpred P[ object, object, object] means ex D2 be set st D2 = $2 & for sf be Subset-Family of (M . $3) holds for Fi be non empty set st Fi = (D . $3) & sf = { z where z be Element of Fi : D2 c= z } holds $1 = ( Intersect sf);

       A1:

      now

        consider K be ManySortedSet of I such that

         A2: K in G by PBOOLE: 134;

        let i be object such that

         A3: i in I;

        reconsider b = (( bool M) . i) as non empty set by A3;

        let x be object such that

         A4: x in (G . i);

        ( dom (K +* (i .--> x))) = I by A3, PZFMISC1: 1;

        then

        reconsider X = (K +* (i .--> x)) as ManySortedSet of I by PARTFUN1:def 2, RELAT_1:def 18;

        

         A5: ( dom (i .--> x)) = {i};

        i in {i} by TARSKI:def 1;

        

        then

         A6: (X . i) = ((i .--> x) . i) by A5, FUNCT_4: 13

        .= x by FUNCOP_1: 72;

        

         A7: X is Element of ( bool M)

        proof

          let s be object such that

           A8: s in I;

          per cases ;

            suppose s = i;

            hence thesis by A4, A6;

          end;

            suppose s <> i;

            then not s in ( dom (i .--> x)) by TARSKI:def 1;

            then (X . s) = (K . s) by FUNCT_4: 11;

            hence thesis by A2, A8;

          end;

        end;

        then

        consider SF be non-empty MSSubsetFamily of M such that

         A9: for Y be ManySortedSet of I holds Y in SF iff Y in D & X c= Y by Th31;

        reconsider sf = (SF . i) as Subset-Family of (M . i) by A3, MSSUBFAM: 32;

        reconsider q = ( Intersect sf) as Element of b by A3, MBOOLEAN:def 1;

        reconsider s = (b --> q) as Function of b, b;

        reconsider y = (s . x) as object;

        take y;

        ( Intersect sf) in ( bool (M . i));

        then ( Intersect sf) in b by A3, MBOOLEAN:def 1;

        hence y in (G . i) by A4, FUNCOP_1: 7;

        thus P[y, x, i]

        proof

          reconsider Di = (D . i) as non empty set by A3;

          

           A10: (SF . i) = { z where z be Element of Di : (X . i) c= z } by A3, A7, A9, Th32;

          reconsider xx = x as set by TARSKI: 1;

          take xx;

          thus xx = x;

          let sf1 be Subset-Family of (M . i), Fi be non empty set;

          assume Fi = (D . i) & sf1 = { z where z be Element of Fi : xx c= z };

          hence thesis by A4, A6, A10, FUNCOP_1: 7;

        end;

      end;

      consider J be ManySortedFunction of G, G such that

       A11: for i be object st i in I holds ex f be Function of (G . i), (G . i) st f = (J . i) & for x be object st x in (G . i) holds P[(f . x), x, i] from MSSUBFAM:sch 1( A1);

      reconsider J as MSSetOp of M;

      take J;

      let X be Element of ( bool M), SF be non-empty MSSubsetFamily of M such that

       A12: for Y be ManySortedSet of I holds Y in SF iff Y in D & X c= Y;

      now

        let i be object;

        assume

         A13: i in I;

        then

        consider Q be Subset-Family of (M . i) such that

         A14: Q = (SF . i) and

         A15: (( meet SF) . i) = ( Intersect Q) by MSSUBFAM:def 1;

        reconsider Fi = (D . i) as non empty set by A13;

        

         A16: Q = { z where z be Element of Fi : (X . i) c= z } by A12, A13, A14, Th32;

        X in G by MSSUBFAM: 12;

        then

         A17: (X . i) in (G . i) by A13;

        consider f be Function of (G . i), (G . i) such that

         A18: f = (J . i) and

         A19: for x be object st x in (G . i) holds P[(f . x), x, i] by A11, A13;

        

         A20: P[(f . (X . i)), (X . i), i] by A19, A17;

        

        thus ((J .. X) . i) = (f . (X . i)) by A13, A18, PRALG_1:def 20

        .= (( meet SF) . i) by A15, A16, A20;

      end;

      hence thesis;

    end;

    theorem :: CLOSURE1:34

    

     Th34: for D be properly-upper-bound MSSubsetFamily of M holds for A be Element of ( bool M) holds for J be MSSetOp of M st A in D & for X be Element of ( bool M) holds for SF be non-empty MSSubsetFamily of M st (for Y be ManySortedSet of I holds Y in SF iff Y in D & X c= Y) holds (J .. X) = ( meet SF) holds (J .. A) = A

    proof

      let D be properly-upper-bound MSSubsetFamily of M, A be Element of ( bool M), J be MSSetOp of M such that

       A1: A in D and

       A2: for X be Element of ( bool M) holds for SF be non-empty MSSubsetFamily of M st (for Y be ManySortedSet of I holds Y in SF iff Y in D & X c= Y) holds (J .. X) = ( meet SF);

      consider SF be non-empty MSSubsetFamily of M such that

       A3: for Y be ManySortedSet of I holds Y in SF iff Y in D & A c= Y by Th31;

      A in SF by A1, A3;

      then ( meet SF) c= A by MSSUBFAM: 43;

      then

       A4: (J .. A) c= A by A2, A3;

      

       A5: for Z1 be ManySortedSet of I st Z1 in SF holds A c= Z1 by A3;

      (J .. A) = ( meet SF) by A2, A3;

      then A c= (J .. A) by A5, MSSUBFAM: 45;

      hence (J .. A) = A by A4, PBOOLE: 146;

    end;

    theorem :: CLOSURE1:35

    for D be absolutely-multiplicative MSSubsetFamily of M holds for A be Element of ( bool M) holds for J be MSSetOp of M st (J .. A) = A & for X be Element of ( bool M) holds for SF be non-empty MSSubsetFamily of M st (for Y be ManySortedSet of I holds Y in SF iff Y in D & X c= Y) holds (J .. X) = ( meet SF) holds A in D

    proof

      let D be absolutely-multiplicative MSSubsetFamily of M, A be Element of ( bool M), J be MSSetOp of M such that

       A1: (J .. A) = A and

       A2: for X be Element of ( bool M) holds for SF be non-empty MSSubsetFamily of M st (for Y be ManySortedSet of I holds Y in SF iff Y in D & X c= Y) holds (J .. X) = ( meet SF);

      defpred P[ ManySortedSet of I] means A c= $1;

      consider SF be non-empty MSSubsetFamily of M such that

       A3: for Y be ManySortedSet of I holds Y in SF iff Y in D & A c= Y by Th31;

      

       A4: (for Y be ManySortedSet of I holds Y in SF iff Y in D & P[Y]) implies SF c= D from MSSUBSET;

      (J .. A) = ( meet SF) by A2, A3;

      hence thesis by A1, A3, A4, MSSUBFAM:def 5;

    end;

    theorem :: CLOSURE1:36

    

     Th36: for D be properly-upper-bound MSSubsetFamily of M holds for J be MSSetOp of M st for X be Element of ( bool M) holds for SF be non-empty MSSubsetFamily of M st (for Y be ManySortedSet of I holds Y in SF iff Y in D & X c= Y) holds (J .. X) = ( meet SF) holds J is reflexive monotonic

    proof

      let D be properly-upper-bound MSSubsetFamily of M, J be MSSetOp of M such that

       A1: for X be Element of ( bool M) holds for SF be non-empty MSSubsetFamily of M st (for Y be ManySortedSet of I holds Y in SF iff Y in D & X c= Y) holds (J .. X) = ( meet SF);

      thus J is reflexive

      proof

        let X be Element of ( bool M);

        consider SF be non-empty MSSubsetFamily of M such that

         A2: for Y be ManySortedSet of I holds Y in SF iff Y in D & X c= Y by Th31;

        (J .. X) = ( meet SF) & for Z1 be ManySortedSet of I st Z1 in SF holds X c= Z1 by A1, A2;

        hence thesis by MSSUBFAM: 45;

      end;

      thus J is monotonic

      proof

        let x,y be Element of ( bool M) such that

         A3: x c= y;

        consider SFx be non-empty MSSubsetFamily of M such that

         A4: for Y be ManySortedSet of I holds Y in SFx iff Y in D & x c= Y by Th31;

        consider SFy be non-empty MSSubsetFamily of M such that

         A5: for Y be ManySortedSet of I holds Y in SFy iff Y in D & y c= Y by Th31;

        SFy c= SFx

        proof

          let i be object;

          assume

           A6: i in I;

          then

          consider Fi be non empty set such that

           A7: Fi = (D . i);

          

           A8: (x . i) c= (y . i) by A3, A6;

          (SFx . i) = { t where t be Element of Fi : (x . i) c= t } & (SFy . i) = { z where z be Element of Fi : (y . i) c= z } by A4, A5, A6, A7, Th32;

          hence thesis by A8, Th1;

        end;

        then

         A9: ( meet SFx) c= ( meet SFy) by MSSUBFAM: 46;

        (J .. x) = ( meet SFx) by A1, A4;

        hence thesis by A1, A5, A9;

      end;

    end;

    theorem :: CLOSURE1:37

    

     Th37: for D be absolutely-multiplicative MSSubsetFamily of M holds for J be MSSetOp of M st for X be Element of ( bool M) holds for SF be non-empty MSSubsetFamily of M st (for Y be ManySortedSet of I holds Y in SF iff Y in D & X c= Y) holds (J .. X) = ( meet SF) holds J is idempotent

    proof

      let D be absolutely-multiplicative MSSubsetFamily of M, J be MSSetOp of M such that

       A1: for X be Element of ( bool M) holds for SF be non-empty MSSubsetFamily of M st (for Y be ManySortedSet of I holds Y in SF iff Y in D & X c= Y) holds (J .. X) = ( meet SF);

      let X be Element of ( bool M);

      defpred P[ ManySortedSet of I] means X c= $1;

      consider SF be non-empty MSSubsetFamily of M such that

       A2: for Y be ManySortedSet of I holds Y in SF iff Y in D & X c= Y by Th31;

      (for Y be ManySortedSet of I holds Y in SF iff Y in D & P[Y]) implies SF c= D from MSSUBSET;

      then

       A3: ( meet SF) in D by A2, MSSUBFAM:def 5;

      D c= ( bool M) by PBOOLE:def 18;

      then

       A4: ( meet SF) is Element of ( bool M) by A3, MSSUBFAM: 11, PBOOLE: 9;

      

      thus (J .. X) = ( meet SF) by A1, A2

      .= (J .. ( meet SF)) by A1, A3, A4, Th34

      .= (J .. (J .. X)) by A1, A2;

    end;

    theorem :: CLOSURE1:38

    for D be MSClosureSystem of S holds for J be MSSetOp of the Sorts of D st for X be Element of ( bool the Sorts of D) holds for SF be non-empty MSSubsetFamily of the Sorts of D st (for Y be ManySortedSet of the carrier of S holds Y in SF iff Y in the Family of D & X c= Y) holds (J .. X) = ( meet SF) holds J is MSClosureOperator of the Sorts of D by Th36, Th37;

    definition

      let S;

      let A be ManySortedSet of the carrier of S;

      let C be MSClosureOperator of A;

      :: CLOSURE1:def13

      func ClOp->ClSys C -> MSClosureSystem of S means

      : Def13: ex D be MSSubsetFamily of A st D = ( MSFixPoints C) & it = MSClosureStr (# A, D #);

      existence

      proof

        reconsider D = ( MSFixPoints C) as MSSubsetFamily of A;

        reconsider a = MSClosureStr (# A, D #) as MSClosureSystem of S by Th30;

        take a;

        thus thesis;

      end;

      uniqueness ;

    end

    registration

      let S;

      let A be ManySortedSet of the carrier of S;

      let C be MSClosureOperator of A;

      cluster ( ClOp->ClSys C) -> strict;

      coherence

      proof

        ex D be MSSubsetFamily of A st D = ( MSFixPoints C) & ( ClOp->ClSys C) = MSClosureStr (# A, D #) by Def13;

        hence thesis;

      end;

    end

    registration

      let S;

      let A be non-empty ManySortedSet of the carrier of S;

      let C be MSClosureOperator of A;

      cluster ( ClOp->ClSys C) -> non-empty;

      coherence

      proof

        ex D be MSSubsetFamily of A st D = ( MSFixPoints C) & ( ClOp->ClSys C) = MSClosureStr (# A, D #) by Def13;

        hence thesis;

      end;

    end

    definition

      let S;

      let D be MSClosureSystem of S;

      :: CLOSURE1:def14

      func ClSys->ClOp D -> MSClosureOperator of the Sorts of D means

      : Def14: for X be Element of ( bool the Sorts of D) holds for SF be non-empty MSSubsetFamily of the Sorts of D st (for Y be ManySortedSet of the carrier of S holds Y in SF iff Y in the Family of D & X c= Y) holds (it .. X) = ( meet SF);

      existence

      proof

        consider J be MSSetOp of the Sorts of D such that

         A1: for X be Element of ( bool the Sorts of D) holds for SF be non-empty MSSubsetFamily of the Sorts of D st (for Y be ManySortedSet of the carrier of S holds Y in SF iff Y in the Family of D & X c= Y) holds (J .. X) = ( meet SF) by Th33;

        reconsider J as MSClosureOperator of the Sorts of D by A1, Th36, Th37;

        take J;

        thus thesis by A1;

      end;

      uniqueness

      proof

        set M = the Sorts of D;

        let Q1,Q2 be MSClosureOperator of the Sorts of D such that

         A2: for X be Element of ( bool the Sorts of D) holds for SF be non-empty MSSubsetFamily of the Sorts of D st (for Y be ManySortedSet of the carrier of S holds Y in SF iff Y in the Family of D & X c= Y) holds (Q1 .. X) = ( meet SF) and

         A3: for X be Element of ( bool the Sorts of D) holds for SF be non-empty MSSubsetFamily of the Sorts of D st (for Y be ManySortedSet of the carrier of S holds Y in SF iff Y in the Family of D & X c= Y) holds (Q2 .. X) = ( meet SF);

        now

          let x be ManySortedSet of the carrier of S;

          assume x in ( bool M);

          then

           A4: x is Element of ( bool M) by MSSUBFAM: 11;

          then

          consider SF be non-empty MSSubsetFamily of the Sorts of D such that

           A5: for Y be ManySortedSet of the carrier of S holds Y in SF iff Y in the Family of D & x c= Y by Th31;

          

          thus (Q1 .. x) = ( meet SF) by A2, A4, A5

          .= (Q2 .. x) by A3, A4, A5;

        end;

        hence Q1 = Q2 by Th7;

      end;

    end

    theorem :: CLOSURE1:39

    for A be ManySortedSet of the carrier of S holds for J be MSClosureOperator of A holds ( ClSys->ClOp ( ClOp->ClSys J)) = J

    proof

      let A be ManySortedSet of the carrier of S, J be MSClosureOperator of A;

      set I = the carrier of S, M = the Sorts of ( ClOp->ClSys J), j = ( ClSys->ClOp ( ClOp->ClSys J));

      

       A1: ex D be MSSubsetFamily of A st D = ( MSFixPoints J) & ( ClOp->ClSys J) = MSClosureStr (# A, D #) by Def13;

      for X be ManySortedSet of I st X in ( bool A) holds (j .. X) = (J .. X)

      proof

        let X be ManySortedSet of I;

        assume X in ( bool A);

        then

         A2: X is Element of ( bool M) by A1, MSSUBFAM: 11;

        then

        consider SF be non-empty MSSubsetFamily of M such that

         A3: for Y be ManySortedSet of I holds Y in SF iff Y in ( MSFixPoints J) & X c= Y by A1, Th31;

        now

          let i be object such that

           A5: i in I;

          reconsider f = (J . i) as Function of (( bool A) . i), (( bool A) . i) by A5, PBOOLE:def 15;

          (( bool A) . i) = ( bool (A . i)) by A5, MBOOLEAN:def 1;

          then

          reconsider f as Function of ( bool (A . i)), ( bool (A . i));

          (X . i) is Element of (( bool A) . i) by A1, A2, A5, PBOOLE:def 14;

          then

           A6: (X . i) is Element of ( bool (A . i)) by A5, MBOOLEAN:def 1;

          then

           A7: (X . i) c= (f . (X . i)) by A5, Th24;

          reconsider Di = (( MSFixPoints J) . i) as non empty set by A1, A5;

          consider Q be Subset-Family of (M . i) such that

           A8: Q = (SF . i) and

           A9: (( meet SF) . i) = ( Intersect Q) by A5, MSSUBFAM:def 1;

          

           A10: (SF . i) = { z where z be Element of Di : (X . i) c= z } by A1, A2, A3, A5, Th32;

          now

            let x;

            assume x in Q;

            then

            consider x1 be Element of Di such that

             A11: x1 = x & (X . i) c= x1 by A8, A10;

            ( MSFixPoints J) c= ( bool A) by PBOOLE:def 18;

            then Di c= (( bool A) . i) by A5;

            then Di c= ( bool (A . i)) by A5, MBOOLEAN:def 1;

            then

             A12: x1 is Element of ( bool (A . i));

            ex g be Function st g = (J . i) & x1 in ( dom g) & (g . x1) = x1 by A5, Def12;

            hence (f . (X . i)) c= x by A5, A6, A11, A12, Th25;

          end;

          then

           A13: (f . (X . i)) c= ( Intersect Q) by A5, A8, MSSUBFAM: 5;

          

           A14: ( dom f) = ( bool (A . i)) & (f . (X . i)) in ( bool (A . i)) by A6, FUNCT_2: 5, FUNCT_2:def 1;

          (f . (f . (X . i))) = (f . (X . i)) by A5, A6, Th26;

          then (f . (X . i)) is Element of Di by A5, A14, Def12;

          then (f . (X . i)) in { z where z be Element of Di : (X . i) c= z } by A7;

          then ( Intersect Q) c= (f . (X . i)) by A8, A10, MSSUBFAM: 2;

          then ( Intersect Q) = (f . (X . i)) by A13;

          

          hence ((j .. X) . i) = (f . (X . i)) by A1, A2, A3, A9, Def14

          .= ((J .. X) . i) by A5, PRALG_1:def 20;

        end;

        hence thesis;

      end;

      hence thesis by A1, Th7;

    end;

    theorem :: CLOSURE1:40

    for D be MSClosureSystem of S holds ( ClOp->ClSys ( ClSys->ClOp D)) = the MSClosureStr of D

    proof

      let D be MSClosureSystem of S;

      set M = the Sorts of D, F = the Family of D, I = the carrier of S;

      consider X1 be ManySortedSet of I such that

       A1: X1 in ( bool M) by PBOOLE: 134;

      F = ( MSFixPoints ( ClSys->ClOp D))

      proof

        let i be object such that

         A3: i in I;

        reconsider f = (( ClSys->ClOp D) . i) as Function of (( bool M) . i), (( bool M) . i) by A3, PBOOLE:def 15;

        reconsider Fi = (F . i) as non empty set by A3;

        thus (F . i) c= (( MSFixPoints ( ClSys->ClOp D)) . i)

        proof

          let x be object such that

           A4: x in (F . i);

          reconsider xx = x as set by TARSKI: 1;

          ( dom (X1 +* (i .--> x))) = I by A3, PZFMISC1: 1;

          then

          reconsider X = (X1 +* (i .--> x)) as ManySortedSet of I by PARTFUN1:def 2, RELAT_1:def 18;

          

           A5: ( dom (i .--> x)) = {i};

          F c= ( bool M) by PBOOLE:def 18;

          then

           A6: (F . i) c= (( bool M) . i) by A3;

          then x in (( bool M) . i) by A4;

          then

           A7: x in ( dom f) by FUNCT_2:def 1;

          i in {i} by TARSKI:def 1;

          

          then

           A8: (X . i) = ((i .--> x) . i) by A5, FUNCT_4: 13

          .= x by FUNCOP_1: 72;

          X is Element of ( bool M)

          proof

            let s be object such that

             A9: s in I;

            per cases ;

              suppose s = i;

              hence thesis by A4, A8, A6;

            end;

              suppose s <> i;

              then not s in ( dom (i .--> x)) by TARSKI:def 1;

              then (X . s) = (X1 . s) by FUNCT_4: 11;

              hence thesis by A1, A9;

            end;

          end;

          then

          reconsider X as Element of ( bool M);

          consider SF be non-empty MSSubsetFamily of M such that

           A10: for Y be ManySortedSet of I holds Y in SF iff Y in F & X c= Y by Th31;

          consider Q be Subset-Family of (M . i) such that

           A11: Q = (SF . i) and

           A12: (( meet SF) . i) = ( Intersect Q) by A3, MSSUBFAM:def 1;

          

           A13: (SF . i) = { z where z be Element of Fi : (X . i) c= z } by A3, A10, Th32;

          now

            let Z1 be set;

            assume Z1 in Q;

            then ex q be Element of Fi st q = Z1 & (X . i) c= q by A11, A13;

            hence xx c= Z1 by A8;

          end;

          then

           A14: xx c= ( Intersect Q) by A3, A11, MSSUBFAM: 5;

          x in { B where B be Element of Fi : xx c= B } by A4;

          then ( Intersect Q) c= xx by A8, A11, A13, MSSUBFAM: 2;

          then

           A15: ( Intersect Q) = x by A14, XBOOLE_0:def 10;

          (( ClSys->ClOp D) .. X) = ( meet SF) by A10, Def14;

          then (f . x) = x by A3, A8, A12, A15, PRALG_1:def 20;

          hence thesis by A3, A7, Def12;

        end;

        let x be object;

        assume

         A16: x in (( MSFixPoints ( ClSys->ClOp D)) . i);

        then

         A17: ex f be Function st f = (( ClSys->ClOp D) . i) & x in ( dom f) & (f . x) = x by A3, Def12;

        ( dom (X1 +* (i .--> x))) = I by A3, PZFMISC1: 1;

        then

        reconsider X = (X1 +* (i .--> x)) as ManySortedSet of I by PARTFUN1:def 2, RELAT_1:def 18;

        

         A18: ( dom (i .--> x)) = {i};

        i in {i} by TARSKI:def 1;

        

        then

         A19: (X . i) = ((i .--> x) . i) by A18, FUNCT_4: 13

        .= x by FUNCOP_1: 72;

        ( MSFixPoints ( ClSys->ClOp D)) c= ( bool M) by PBOOLE:def 18;

        then

         A20: (( MSFixPoints ( ClSys->ClOp D)) . i) c= (( bool M) . i) by A3;

        X is Element of ( bool M)

        proof

          let s be object such that

           A21: s in I;

          per cases ;

            suppose s = i;

            hence thesis by A16, A19, A20;

          end;

            suppose s <> i;

            then not s in ( dom (i .--> x)) by TARSKI:def 1;

            then (X . s) = (X1 . s) by FUNCT_4: 11;

            hence thesis by A1, A21;

          end;

        end;

        then

        reconsider X as Element of ( bool M);

        defpred P[ ManySortedSet of I] means X c= $1;

        consider SF be non-empty MSSubsetFamily of M such that

         A22: for Y be ManySortedSet of I holds Y in SF iff Y in F & X c= Y by Th31;

        (for Y be ManySortedSet of I holds Y in SF iff Y in F & P[Y]) implies SF c= F from MSSUBSET;

        then

         A24: ( meet SF) in F by A22, MSSUBFAM:def 5;

        (( meet SF) . i) = ((( ClSys->ClOp D) .. X) . i) by A22, Def14

        .= x by A3, A17, A19, PRALG_1:def 20;

        hence thesis by A3, A24;

      end;

      hence thesis by Def13;

    end;