closure2.miz



    begin

    reserve i,x,I for set,

A,B,M for ManySortedSet of I,

f,f1 for Function;

    notation

      let I, A, B;

      synonym A in' B for A in B;

    end

    notation

      let I, A, B;

      synonym A c=' B for A c= B;

    end

    theorem :: CLOSURE2:1

    for M be non empty set holds for X,Y be Element of M st X c= Y holds (( id M) . X) c= (( id M) . Y);

    theorem :: CLOSURE2:2

    

     Th2: for I be non empty set holds for A be ManySortedSet of I holds for B be ManySortedSubset of A holds ( rng B) c= ( union ( rng ( bool A)))

    proof

      let I be non empty set, A be ManySortedSet of I, B be ManySortedSubset of A;

      let a be object;

      assume a in ( rng B);

      then

      consider i be object such that

       A1: i in I and

       A2: a = (B . i) by PBOOLE: 138;

      i in ( dom ( bool A)) & ( bool (A . i)) = (( bool A) . i) by A1, MBOOLEAN:def 1, PARTFUN1:def 2;

      then

       A3: ( bool (A . i)) in ( rng ( bool A)) by FUNCT_1:def 3;

      B c= A by PBOOLE:def 18;

      then B in ( bool A) by MBOOLEAN: 18;

      then (B . i) in (( bool A) . i) by A1;

      then a in ( bool (A . i)) by A1, A2, MBOOLEAN:def 1;

      hence thesis by A3, TARSKI:def 4;

    end;

    begin

    definition

      let I, M;

      defpred f[ object] means $1 is ManySortedSubset of M;

      :: CLOSURE2:def1

      func Bool M -> set means

      : Def1: for x be object holds x in it iff x is ManySortedSubset of M;

      existence

      proof

        per cases ;

          suppose

           A1: I is non empty;

          consider X be set such that

           A2: for e be object holds e in X iff e in ( Funcs (I,( union ( rng ( bool M))))) & f[e] from XBOOLE_0:sch 1;

          take X;

          let x be object;

          thus x in X implies x is ManySortedSubset of M by A2;

          assume

           A3: x is ManySortedSubset of M;

          now

            reconsider xx = x as ManySortedSubset of M by A3;

            ( dom xx) = I & ( rng xx) c= ( union ( rng ( bool M))) by A1, Th2, PARTFUN1:def 2;

            hence x in ( Funcs (I,( union ( rng ( bool M))))) by FUNCT_2:def 2;

            thus f[x] by A3;

          end;

          hence thesis by A2;

        end;

          suppose

           A4: I is empty;

          take {( EmptyMS {} )};

          let x be object;

          thus x in {( EmptyMS {} )} implies x is ManySortedSubset of M

          proof

            reconsider M9 = M as ManySortedSet of {} by A4;

            assume

             A5: x in {( EmptyMS {} )};

            reconsider y = ( EmptyMS {} ) as ManySortedSubset of M9 by PBOOLE:def 18;

            y is ManySortedSubset of M by A4;

            hence thesis by A5, TARSKI:def 1;

          end;

          assume x is ManySortedSubset of M;

          then

          consider y be ManySortedSubset of M such that

           A6: y = x;

          y = ( EmptyMS {} ) by A4;

          hence thesis by A6, TARSKI:def 1;

        end;

      end;

      uniqueness

      proof

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

      end;

    end

    registration

      let I, M;

      cluster ( Bool M) -> non empty functional with_common_domain;

      coherence

      proof

        M is ManySortedSubset of M by PBOOLE:def 18;

        hence ( Bool M) is non empty by Def1;

        thus ( Bool M) is functional by Def1;

        let f,g be Function;

        assume that

         A1: f in ( Bool M) and

         A2: g in ( Bool M);

        

         A3: g is ManySortedSubset of M by A2, Def1;

        f is ManySortedSubset of M by A1, Def1;

        

        hence ( dom f) = I by PARTFUN1:def 2

        .= ( dom g) by A3, PARTFUN1:def 2;

      end;

    end

    definition

      let I, M;

      mode SubsetFamily of M is Subset of ( Bool M);

    end

    definition

      let I, M;

      :: original: Bool

      redefine

      func Bool M -> SubsetFamily of M ;

      coherence

      proof

        ( Bool M) c= ( Bool M);

        hence thesis;

      end;

    end

    registration

      let I, M;

      cluster non empty functional with_common_domain for SubsetFamily of M;

      existence

      proof

        take ( Bool M);

        thus thesis;

      end;

    end

    registration

      let I, M;

      cluster empty finite for SubsetFamily of M;

      existence

      proof

        reconsider x = {} as SubsetFamily of M by XBOOLE_1: 2;

        take x;

        thus thesis;

      end;

    end

    reserve SF,SG for SubsetFamily of M;

    definition

      let I, M;

      let S be non empty SubsetFamily of M;

      :: original: Element

      redefine

      mode Element of S -> ManySortedSubset of M ;

      coherence

      proof

        let e be Element of S;

        thus thesis by Def1;

      end;

    end

    theorem :: CLOSURE2:3

    

     Th3: (SF \/ SG) is SubsetFamily of M;

    theorem :: CLOSURE2:4

    (SF /\ SG) is SubsetFamily of M;

    theorem :: CLOSURE2:5

    (SF \ x) is SubsetFamily of M;

    theorem :: CLOSURE2:6

    (SF \+\ SG) is SubsetFamily of M;

    theorem :: CLOSURE2:7

    

     Th7: A c= M implies {A} is SubsetFamily of M

    proof

      assume A c= M;

      then A is ManySortedSubset of M by PBOOLE:def 18;

      then A in ( Bool M) by Def1;

      hence thesis by ZFMISC_1: 31;

    end;

    theorem :: CLOSURE2:8

    

     Th8: A c= M & B c= M implies {A, B} is SubsetFamily of M

    proof

      assume A c= M & B c= M;

      then {A} is SubsetFamily of M & {B} is SubsetFamily of M by Th7;

      then ( {A} \/ {B}) is SubsetFamily of M by Th3;

      hence thesis by ENUMSET1: 1;

    end;

    reserve E,T for Element of ( Bool M);

    theorem :: CLOSURE2:9

    

     Th9: (E (/\) T) in ( Bool M)

    proof

      E c= M & T c= M by PBOOLE:def 18;

      then (E (/\) T) c= (M (/\) M) by PBOOLE: 21;

      then (E (/\) T) is ManySortedSubset of M by PBOOLE:def 18;

      hence thesis by Def1;

    end;

    theorem :: CLOSURE2:10

    

     Th10: (E (\/) T) in ( Bool M)

    proof

      E c= M & T c= M by PBOOLE:def 18;

      then (E (\/) T) c= (M (\/) M) by PBOOLE: 20;

      then (E (\/) T) is ManySortedSubset of M by PBOOLE:def 18;

      hence thesis by Def1;

    end;

    theorem :: CLOSURE2:11

    (E (\) A) in ( Bool M)

    proof

      E c= M by PBOOLE:def 18;

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

      then (E (\) A) is ManySortedSubset of M by PBOOLE:def 18;

      hence thesis by Def1;

    end;

    theorem :: CLOSURE2:12

    (E (\+\) T) in ( Bool M)

    proof

      T c= M by PBOOLE:def 18;

      then

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

      E c= M by PBOOLE:def 18;

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

      then (E (\+\) T) c= M by A1, PBOOLE: 91;

      then (E (\+\) T) is ManySortedSubset of M by PBOOLE:def 18;

      hence thesis by Def1;

    end;

    begin

    definition

      let S be functional set;

      :: CLOSURE2:def2

      func |.S.| -> Function means

      : Def2: ex A be non empty functional set st A = S & ( dom it ) = ( meet the set of all ( dom x) where x be Element of A) & for i st i in ( dom it ) holds (it . i) = the set of all (x . i) where x be Element of A if S <> {}

      otherwise it = {} ;

      existence

      proof

        thus S <> {} implies ex f be Function st ex A be non empty functional set st A = S & ( dom f) = ( meet the set of all ( dom x) where x be Element of A) & for i st i in ( dom f) holds (f . i) = the set of all (x . i) where x be Element of A

        proof

          assume S <> {} ;

          then

          consider A be non empty functional set such that

           A1: A = S;

          deffunc F( object) = the set of all (x . $1) where x be Element of A;

          consider f be Function such that

           A2: ( dom f) = ( meet the set of all ( dom x) where x be Element of A) & for i be object st i in ( meet the set of all ( dom x) where x be Element of A) holds (f . i) = F(i) from FUNCT_1:sch 3;

          take f, A;

          thus thesis by A1, A2;

        end;

        thus thesis;

      end;

      uniqueness

      proof

        let f,g be Function;

        defpred P[ Function] means ex A be non empty functional set st A = S & ( dom $1) = ( meet the set of all ( dom x) where x be Element of A) & for i st i in ( dom $1) holds ($1 . i) = the set of all (x . i) where x be Element of A;

        thus S <> {} & P[f] & P[g] implies f = g

        proof

          assume that S <> {} and

           A3: P[f] and

           A4: P[g];

          consider A be non empty functional set such that

           A5: A = S and

           A6: ( dom f) = ( meet the set of all ( dom x) where x be Element of A) and

           A7: for i st i in ( dom f) holds (f . i) = the set of all (x . i) where x be Element of A by A3;

          now

            let a be object;

            assume

             A8: a in ( meet the set of all ( dom x) where x be Element of A);

            

            hence (f . a) = the set of all (x . a) where x be Element of A by A6, A7

            .= (g . a) by A4, A5, A8;

          end;

          hence thesis by A4, A5, A6;

        end;

        thus thesis;

      end;

      consistency ;

    end

    theorem :: CLOSURE2:13

    

     Th13: for SF be non empty SubsetFamily of M holds ( dom |.SF.|) = I

    proof

      let SF be non empty SubsetFamily of M;

      consider A be non empty functional set such that

       A1: A = SF and

       A2: ( dom |.SF.|) = ( meet the set of all ( dom x) where x be Element of A) and for i st i in ( dom |.SF.|) holds ( |.SF.| . i) = the set of all (x . i) where x be Element of A by Def2;

       the set of all ( dom x) where x be Element of A = {I}

      proof

        thus the set of all ( dom x) where x be Element of A c= {I}

        proof

          let a be object;

          assume a in the set of all ( dom x) where x be Element of A;

          then

          consider x be Element of A such that

           A3: a = ( dom x);

          x is Element of SF by A1;

          then a = I by A3, PARTFUN1:def 2;

          hence thesis by TARSKI:def 1;

        end;

        set x = the Element of A;

        let a be object;

        assume a in {I};

        then

         A4: a = I by TARSKI:def 1;

        x is Element of SF by A1;

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

        hence thesis by A4;

      end;

      hence thesis by A2, SETFAM_1: 10;

    end;

    registration

      let S be empty functional set;

      cluster |.S.| -> empty;

      coherence by Def2;

    end

    definition

      let I, M;

      let S be SubsetFamily of M;

      :: CLOSURE2:def3

      func |:S:| -> ManySortedSet of I equals

      : Def3: |.S.| if S <> {}

      otherwise ( EmptyMS I);

      coherence

      proof

        thus S <> {} implies |.S.| is ManySortedSet of I

        proof

          assume S <> {} ;

          then ( dom |.S.|) = I by Th13;

          hence thesis by PARTFUN1:def 2, RELAT_1:def 18;

        end;

        thus thesis;

      end;

      consistency ;

    end

    registration

      let I, M;

      let S be empty SubsetFamily of M;

      cluster |:S:| -> empty-yielding;

      coherence

      proof

         |:S:| = ( EmptyMS I) by Def3;

        hence thesis;

      end;

    end

    theorem :: CLOSURE2:14

    

     Th14: SF is non empty implies for i st i in I holds ( |:SF:| . i) = { (x . i) where x be Element of ( Bool M) : x in SF }

    proof

      

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

      assume

       A2: SF is non empty;

      then

      consider A be non empty functional set such that

       A3: A = SF and ( dom |.SF.|) = ( meet the set of all ( dom x) where x be Element of A) and

       A4: for i st i in ( dom |.SF.|) holds ( |.SF.| . i) = the set of all (x . i) where x be Element of A by Def2;

      let i such that

       A5: i in I;

      set K = { (x . i) where x be Element of ( Bool M) : x in SF }, N = the set of all (x . i) where x be Element of A;

      

       A6: K = N

      proof

        thus K c= N

        proof

          let q be object;

          assume q in K;

          then ex x be Element of ( Bool M) st q = (x . i) & x in SF;

          hence thesis by A3;

        end;

        let q be object;

        assume q in N;

        then

        consider x be Element of A such that

         A7: q = (x . i);

        x in SF by A3;

        hence thesis by A7;

      end;

       |:SF:| = |.SF.| by A2, Def3;

      hence thesis by A4, A5, A1, A6;

    end;

    registration

      let I, M;

      let SF be non empty SubsetFamily of M;

      cluster |:SF:| -> non-empty;

      coherence

      proof

        let i be object;

        assume i in I;

        then

         A1: ( |:SF:| . i) = { (x . i) where x be Element of ( Bool M) : x in SF } by Th14;

        consider x be object such that

         A2: x in SF by XBOOLE_0:def 1;

        reconsider x as Element of ( Bool M) by A2;

        (x . i) in ( |:SF:| . i) by A1, A2;

        hence thesis;

      end;

    end

    theorem :: CLOSURE2:15

    

     Th15: ( dom |. {f}.|) = ( dom f)

    proof

      consider A be non empty functional set such that

       A1: A = {f} and

       A2: ( dom |. {f}.|) = ( meet the set of all ( dom x) where x be Element of A) and for i st i in ( dom |. {f}.|) holds ( |. {f}.| . i) = the set of all (x . i) where x be Element of A by Def2;

      set m = the set of all ( dom x) where x be Element of A;

      m = {( dom f)}

      proof

        thus m c= {( dom f)}

        proof

          let q be object;

          assume q in m;

          then

          consider x be Element of A such that

           A3: q = ( dom x);

          x = f by A1, TARSKI:def 1;

          hence thesis by A3, TARSKI:def 1;

        end;

        let q be object;

        assume q in {( dom f)};

        then

         A4: q = ( dom f) by TARSKI:def 1;

        f is Element of A by A1, TARSKI:def 1;

        hence thesis by A4;

      end;

      hence thesis by A2, SETFAM_1: 10;

    end;

    theorem :: CLOSURE2:16

    ( dom |. {f, f1}.|) = (( dom f) /\ ( dom f1))

    proof

      consider A be non empty functional set such that

       A1: A = {f, f1} and

       A2: ( dom |. {f, f1}.|) = ( meet the set of all ( dom x) where x be Element of A) and for i st i in ( dom |. {f, f1}.|) holds ( |. {f, f1}.| . i) = the set of all (x . i) where x be Element of A by Def2;

      set m = the set of all ( dom x) where x be Element of A;

      m = {( dom f), ( dom f1)}

      proof

        thus m c= {( dom f), ( dom f1)}

        proof

          let q be object;

          assume q in m;

          then

          consider x be Element of A such that

           A3: q = ( dom x);

          x = f or x = f1 by A1, TARSKI:def 2;

          hence thesis by A3, TARSKI:def 2;

        end;

        let q be object;

        assume q in {( dom f), ( dom f1)};

        then

         A4: q = ( dom f) or q = ( dom f1) by TARSKI:def 2;

        f is Element of A & f1 is Element of A by A1, TARSKI:def 2;

        hence thesis by A4;

      end;

      hence thesis by A2, SETFAM_1: 11;

    end;

    theorem :: CLOSURE2:17

    

     Th17: i in ( dom f) implies ( |. {f}.| . i) = {(f . i)}

    proof

      

       A1: f in {f} by TARSKI:def 1;

      consider A be non empty functional set such that

       A2: A = {f} and ( dom |. {f}.|) = ( meet the set of all ( dom x) where x be Element of A) and

       A3: for i st i in ( dom |. {f}.|) holds ( |. {f}.| . i) = the set of all (x . i) where x be Element of A by Def2;

      assume i in ( dom f);

      then i in ( dom |. {f}.|) by Th15;

      then

       A4: ( |. {f}.| . i) = the set of all (x . i) where x be Element of A by A3;

      thus ( |. {f}.| . i) c= {(f . i)}

      proof

        let q be object;

        assume q in ( |. {f}.| . i);

        then

        consider x be Element of A such that

         A5: q = (x . i) by A4;

        x = f by A2, TARSKI:def 1;

        hence thesis by A5, TARSKI:def 1;

      end;

      let q be object;

      assume q in {(f . i)};

      then q = (f . i) by TARSKI:def 1;

      hence thesis by A2, A4, A1;

    end;

    theorem :: CLOSURE2:18

    i in I & SF = {f} implies ( |:SF:| . i) = {(f . i)}

    proof

      assume that

       A1: i in I and

       A2: SF = {f};

      

       A3: |:SF:| = |.SF.| by A2, Def3;

      ( dom |:SF:|) = I by PARTFUN1:def 2;

      then i in ( dom f) by A1, A2, A3, Th15;

      hence thesis by A2, A3, Th17;

    end;

    theorem :: CLOSURE2:19

    

     Th19: i in ( dom |. {f, f1}.|) implies ( |. {f, f1}.| . i) = {(f . i), (f1 . i)}

    proof

      

       A1: f in {f, f1} & f1 in {f, f1} by TARSKI:def 2;

      consider A be non empty functional set such that

       A2: A = {f, f1} and ( dom |. {f, f1}.|) = ( meet the set of all ( dom x) where x be Element of A) and

       A3: for i st i in ( dom |. {f, f1}.|) holds ( |. {f, f1}.| . i) = the set of all (x . i) where x be Element of A by Def2;

      assume i in ( dom |. {f, f1}.|);

      then

       A4: ( |. {f, f1}.| . i) = the set of all (x . i) where x be Element of A by A3;

      thus ( |. {f, f1}.| . i) c= {(f . i), (f1 . i)}

      proof

        let q be object;

        assume q in ( |. {f, f1}.| . i);

        then

        consider x be Element of A such that

         A5: q = (x . i) by A4;

        per cases by A2, TARSKI:def 2;

          suppose x = f;

          hence thesis by A5, TARSKI:def 2;

        end;

          suppose x = f1;

          hence thesis by A5, TARSKI:def 2;

        end;

      end;

      let q be object;

      assume q in {(f . i), (f1 . i)};

      then q = (f . i) or q = (f1 . i) by TARSKI:def 2;

      hence thesis by A2, A4, A1;

    end;

    theorem :: CLOSURE2:20

    

     Th20: i in I & SF = {f, f1} implies ( |:SF:| . i) = {(f . i), (f1 . i)}

    proof

      assume that

       A1: i in I and

       A2: SF = {f, f1};

      ( dom |:SF:|) = I & |:SF:| = |.SF.| by A2, Def3, PARTFUN1:def 2;

      hence thesis by A1, A2, Th19;

    end;

    definition

      let I, M, SF;

      :: original: |:

      redefine

      func |:SF:| -> MSSubsetFamily of M ;

      coherence

      proof

        per cases ;

          suppose

           A1: SF is non empty;

           |:SF:| is ManySortedSubset of ( bool M)

          proof

            let i be object;

            assume

             A2: i in I;

            then

             A3: ( |:SF:| . i) = { (x . i) where x be Element of ( Bool M) : x in SF } by A1, Th14;

            thus ( |:SF:| . i) c= (( bool M) . i)

            proof

              let x be object;

              assume x in ( |:SF:| . i);

              then

              consider a be Element of ( Bool M) such that

               A4: x = (a . i) and a in SF by A3;

              a c= M by PBOOLE:def 18;

              then (a . i) c= (M . i) by A2;

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

              hence thesis by A2, MBOOLEAN:def 1;

            end;

          end;

          hence thesis;

        end;

          suppose SF is empty;

          then |:SF:| = ( EmptyMS I);

          hence thesis by MSSUBFAM: 31;

        end;

      end;

    end

    theorem :: CLOSURE2:21

    

     Th21: A in SF implies A in' |:SF:|

    proof

      assume

       A1: A in SF;

      let i be object;

      assume i in I;

      then ( |:SF:| . i) = { (x . i) where x be Element of ( Bool M) : x in SF } by A1, Th14;

      hence thesis by A1;

    end;

    theorem :: CLOSURE2:22

    

     Th22: SF = {A, B} implies ( union |:SF:|) = (A (\/) B)

    proof

      assume

       A1: SF = {A, B};

      now

        let i be object;

        assume

         A2: i in I;

        

        hence (( union |:SF:|) . i) = ( union ( |:SF:| . i)) by MBOOLEAN:def 2

        .= ( union {(A . i), (B . i)}) by A1, A2, Th20

        .= ((A . i) \/ (B . i)) by ZFMISC_1: 75

        .= ((A (\/) B) . i) by A2, PBOOLE:def 4;

      end;

      hence thesis;

    end;

    theorem :: CLOSURE2:23

    

     Th23: SF = {E, T} implies ( meet |:SF:|) = (E (/\) T)

    proof

      assume

       A1: SF = {E, T};

      now

        reconsider sf1 = SF as non empty SubsetFamily of M by A1;

        let i be object such that

         A2: i in I;

        ex Q be Subset-Family of (M . i) st Q = ( |:sf1:| . i) & (( meet |:sf1:|) . i) = ( Intersect Q) by A2, MSSUBFAM:def 1;

        

        hence (( meet |:SF:|) . i) = ( meet ( |:sf1:| . i)) by A2, SETFAM_1:def 9

        .= ( meet {(E . i), (T . i)}) by A1, A2, Th20

        .= ((E . i) /\ (T . i)) by SETFAM_1: 11

        .= ((E (/\) T) . i) by A2, PBOOLE:def 5;

      end;

      hence thesis;

    end;

    theorem :: CLOSURE2:24

    

     Th24: for Z be ManySortedSubset of M st for Z1 be ManySortedSet of I st Z1 in SF holds Z c=' Z1 holds Z c=' ( meet |:SF:|)

    proof

      let Z be ManySortedSubset of M such that

       A1: for Z1 be ManySortedSet of I st Z1 in SF holds Z c=' Z1;

      let i be object such that

       A2: i in I;

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

       A3: Q = ( |:SF:| . i) and

       A4: (( meet |:SF:|) . i) = ( Intersect Q) by A2, MSSUBFAM:def 1;

       A5:

      now

        let q be set such that

         A6: q in Q;

        per cases ;

          suppose SF is non empty;

          then ( |:SF:| . i) = { (x . i) where x be Element of ( Bool M) : x in SF } by A2, Th14;

          then

          consider a be Element of ( Bool M) such that

           A7: q = (a . i) and

           A8: a in SF by A3, A6;

          Z c=' a by A1, A8;

          hence (Z . i) c= q by A2, A7;

        end;

          suppose SF is empty;

          then |:SF:| = ( EmptyMS I);

          hence (Z . i) c= q by A3, A6;

        end;

      end;

      Z c= M by PBOOLE:def 18;

      then (Z . i) is Subset of (M . i) by A2;

      hence thesis by A4, A5, MSSUBFAM: 4;

    end;

    theorem :: CLOSURE2:25

     |:( Bool M):| = ( bool M)

    proof

      now

        let i be object;

        assume

         A1: i in I;

        then

         A2: ( |:( Bool M):| . i) = { (x . i) where x be Element of ( Bool M) : x in ( Bool M) } by Th14;

        thus ( |:( Bool M):| . i) = (( bool M) . i)

        proof

          thus ( |:( Bool M):| . i) c= (( bool M) . i) by A1, PBOOLE:def 2, PBOOLE:def 18;

          let a be object such that

           A3: a in (( bool M) . i);

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

          then

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

          

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

          i in {i} by TARSKI:def 1;

          

          then

           A5: (X . i) = ((i .--> a) . i) by A4, FUNCT_4: 13

          .= a by FUNCOP_1: 72;

          X is ManySortedSubset of M

          proof

            let s be object such that

             A6: s in I;

            per cases ;

              suppose

               A7: s = i;

              then a in ( bool (M . s)) by A3, A6, MBOOLEAN:def 1;

              hence thesis by A5, A7;

            end;

              suppose s <> i;

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

              

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

              .= {} ;

              hence thesis;

            end;

          end;

          then X is Element of ( Bool M) by Def1;

          hence thesis by A2, A5;

        end;

      end;

      hence thesis;

    end;

    definition

      let I, M;

      let IT be SubsetFamily of M;

      :: CLOSURE2:def4

      attr IT is additive means for A, B st A in IT & B in IT holds (A (\/) B) in IT;

      :: CLOSURE2:def5

      attr IT is absolutely-additive means for F be SubsetFamily of M st F c= IT holds ( union |:F:|) in IT;

      :: CLOSURE2:def6

      attr IT is multiplicative means for A, B st A in IT & B in IT holds (A (/\) B) in IT;

      :: CLOSURE2:def7

      attr IT is absolutely-multiplicative means

      : Def7: for F be SubsetFamily of M st F c= IT holds ( meet |:F:|) in IT;

      :: CLOSURE2:def8

      attr IT is properly-upper-bound means

      : Def8: M in IT;

      :: CLOSURE2:def9

      attr IT is properly-lower-bound means ( EmptyMS I) in IT;

    end

    

     Lm1: ( Bool M) is additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound

    proof

      thus ( Bool M) is additive by Th10;

      thus ( Bool M) is absolutely-additive

      proof

        let F be SubsetFamily of M such that F c= ( Bool M);

        ( union |:F:|) c= M by MSSUBFAM: 40;

        then ( union |:F:|) is ManySortedSubset of M by PBOOLE:def 18;

        hence thesis by Def1;

      end;

      thus ( Bool M) is multiplicative by Th9;

      thus ( Bool M) is absolutely-multiplicative by Def1;

      M is ManySortedSubset of M by PBOOLE:def 18;

      then M in ( Bool M) by Def1;

      hence ( Bool M) is properly-upper-bound;

      ( EmptyMS I) c= M by PBOOLE: 43;

      then ( EmptyMS I) is ManySortedSubset of M by PBOOLE:def 18;

      hence ( EmptyMS I) in ( Bool M) by Def1;

    end;

    registration

      let I, M;

      cluster non empty functional with_common_domain additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound for SubsetFamily of M;

      existence

      proof

        take ( Bool M);

        thus thesis by Lm1;

      end;

    end

    definition

      let I, M;

      :: original: Bool

      redefine

      func Bool M -> additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound SubsetFamily of M ;

      coherence by Lm1;

    end

    registration

      let I, M;

      cluster absolutely-additive -> additive for SubsetFamily of M;

      coherence

      proof

        let SF be SubsetFamily of M such that

         A1: SF is absolutely-additive;

        let A, B;

        assume that

         A2: A in SF and

         A3: B in SF;

        B is ManySortedSubset of M by A3, Def1;

        then

         A4: B c= M by PBOOLE:def 18;

        A is ManySortedSubset of M by A2, Def1;

        then A c= M by PBOOLE:def 18;

        then

        reconsider ab = {A, B} as SubsetFamily of M by A4, Th8;

         {A} c= SF & {B} c= SF by A2, A3, ZFMISC_1: 31;

        then ( {A} \/ {B}) c= SF by XBOOLE_1: 8;

        then {A, B} c= SF by ENUMSET1: 1;

        then ( union |:ab:|) in SF by A1;

        hence thesis by Th22;

      end;

    end

    registration

      let I, M;

      cluster absolutely-multiplicative -> multiplicative for SubsetFamily of M;

      coherence

      proof

        let SF be SubsetFamily of M such that

         A1: SF is absolutely-multiplicative;

        let A, B;

        assume that

         A2: A in SF and

         A3: B in SF;

        B is ManySortedSubset of M by A3, Def1;

        then

         A4: B c= M by PBOOLE:def 18;

        A is ManySortedSubset of M by A2, Def1;

        then A c= M by PBOOLE:def 18;

        then

        reconsider ab = {A, B} as SubsetFamily of M by A4, Th8;

         {A} c= SF & {B} c= SF by A2, A3, ZFMISC_1: 31;

        then ( {A} \/ {B}) c= SF by XBOOLE_1: 8;

        then {A, B} c= SF by ENUMSET1: 1;

        then ( meet |:ab:|) in SF by A1;

        hence thesis by A2, A3, Th23;

      end;

    end

    registration

      let I, M;

      cluster absolutely-multiplicative -> properly-upper-bound for SubsetFamily of M;

      coherence

      proof

        reconsider a = {} as SubsetFamily of M by XBOOLE_1: 2;

        let SF be SubsetFamily of M such that

         A1: SF is absolutely-multiplicative;

         |:a:| = ( EmptyMS I);

        then

         A2: ( meet |:a:|) = M by MSSUBFAM: 41;

        a c= SF;

        hence M in SF by A1, A2;

      end;

    end

    registration

      let I, M;

      cluster properly-upper-bound -> non empty for SubsetFamily of M;

      coherence ;

    end

    registration

      let I, M;

      cluster absolutely-additive -> properly-lower-bound for SubsetFamily of M;

      coherence

      proof

        reconsider a = {} as SubsetFamily of M by XBOOLE_1: 2;

        let SF be SubsetFamily of M such that

         A1: SF is absolutely-additive;

         |:a:| = ( EmptyMS I);

        then

         A2: ( union |:a:|) = ( EmptyMS I) by MBOOLEAN: 21;

        a c= SF;

        hence ( EmptyMS I) in SF by A1, A2;

      end;

    end

    registration

      let I, M;

      cluster properly-lower-bound -> non empty for SubsetFamily of M;

      coherence ;

    end

    begin

    definition

      let I, M;

      mode SetOp of M is Function of ( Bool M), ( Bool M);

    end

    definition

      let I, M;

      let f be SetOp of M;

      let x be Element of ( Bool M);

      :: original: .

      redefine

      func f . x -> Element of ( Bool M) ;

      coherence

      proof

        (f . x) in ( Bool M);

        hence thesis;

      end;

    end

    definition

      let I, M;

      let IT be SetOp of M;

      :: CLOSURE2:def10

      attr IT is reflexive means

      : Def10: for x be Element of ( Bool M) holds x c=' (IT . x);

      :: CLOSURE2:def11

      attr IT is monotonic means

      : Def11: for x,y be Element of ( Bool M) st x c=' y holds (IT . x) c=' (IT . y);

      :: CLOSURE2:def12

      attr IT is idempotent means

      : Def12: for x be Element of ( Bool M) holds (IT . x) = (IT . (IT . x));

      :: CLOSURE2:def13

      attr IT is topological means for x,y be Element of ( Bool M) holds (IT . (x (\/) y)) = ((IT . x) (\/) (IT . y));

    end

    registration

      let I, M;

      cluster reflexive monotonic idempotent topological for SetOp of M;

      existence

      proof

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

        take f;

        thus f is reflexive;

        thus f is monotonic;

        thus f is idempotent;

        thus f is topological

        proof

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

          X c= M & Y c= M by PBOOLE:def 18;

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

          then (X (\/) Y) is ManySortedSubset of M by PBOOLE:def 18;

          then (X (\/) Y) in ( Bool M) by Def1;

          

          hence (f . (X (\/) Y)) = (X (\/) Y) by FUNCT_1: 18

          .= ((f . X) (\/) Y)

          .= ((f . X) (\/) (f . Y));

        end;

      end;

    end

    theorem :: CLOSURE2:26

    ( id ( Bool A)) is reflexive SetOp of A

    proof

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

      f is reflexive;

      hence thesis;

    end;

    theorem :: CLOSURE2:27

    ( id ( Bool A)) is monotonic SetOp of A

    proof

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

      f is monotonic;

      hence thesis;

    end;

    theorem :: CLOSURE2:28

    ( id ( Bool A)) is idempotent SetOp of A

    proof

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

      f is idempotent;

      hence thesis;

    end;

    theorem :: CLOSURE2:29

    ( id ( Bool A)) is topological SetOp of A

    proof

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

      f is topological

      proof

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

        X c= A & Y c= A by PBOOLE:def 18;

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

        then (X (\/) Y) is ManySortedSubset of A by PBOOLE:def 18;

        then (X (\/) Y) in ( Bool A) by Def1;

        

        hence (f . (X (\/) Y)) = (X (\/) Y) by FUNCT_1: 18

        .= ((f . X) (\/) Y)

        .= ((f . X) (\/) (f . Y));

      end;

      hence thesis;

    end;

    reserve g,h for SetOp of M;

    theorem :: CLOSURE2:30

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

    proof

      assume

       A1: E = M;

      assume g is reflexive;

      then

       A2: E c= (g . E);

      (g . E) c= E by A1, PBOOLE:def 18;

      hence thesis by A2, PBOOLE: 146;

    end;

    theorem :: CLOSURE2:31

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

    proof

      assume that

       A1: g is reflexive and

       A2: for X be Element of ( Bool M) holds (g . X) c= X;

      let X be Element of ( Bool M);

      

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

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

      hence thesis by A3, PBOOLE: 146;

    end;

    theorem :: CLOSURE2:32

    for A be Element of ( Bool M) st A = (E (/\) T) holds g is monotonic implies (g . A) c= ((g . E) (/\) (g . T))

    proof

      let A be Element of ( Bool M) such that

       A1: A = (E (/\) T);

      assume

       A2: g is monotonic;

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

      then

       A3: (g . A) c= (g . T) by A1, A2;

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

      then (g . A) c= (g . E) by A1, A2;

      hence thesis by A3, PBOOLE: 17;

    end;

    registration

      let I, M;

      cluster topological -> monotonic for SetOp of M;

      coherence

      proof

        let g be SetOp of M such that

         A1: g is topological;

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

         A2: X c= Y;

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

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

        hence thesis by PBOOLE: 26;

      end;

    end

    theorem :: CLOSURE2:33

    for A be Element of ( Bool M) st A = (E (\) T) holds g is topological implies ((g . E) (\) (g . T)) c= (g . A)

    proof

      let A be Element of ( Bool M) such that

       A1: A = (E (\) T);

      assume

       A2: g is topological;

      

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

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

      .= ((g . A) (\/) (g . T)) by A1, A2;

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

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

      then

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

      ((g . A) (\) (g . T)) c= (g . A) by PBOOLE: 56;

      hence thesis by A3, PBOOLE: 13;

    end;

    definition

      let I, M, h, g;

      :: original: *

      redefine

      func g * h -> SetOp of M ;

      coherence

      proof

        (g * h) is Function of ( Bool M), ( Bool M);

        hence thesis;

      end;

    end

    theorem :: CLOSURE2:34

    g is reflexive & h is reflexive implies (g * h) is reflexive

    proof

      assume

       A1: g is reflexive & h is reflexive;

      let X be Element of ( Bool M);

      X c= (h . X) & (h . X) c= (g . (h . X)) by A1;

      then ( dom h) = ( Bool M) & X c= (g . (h . X)) by FUNCT_2:def 1, PBOOLE: 13;

      hence thesis by FUNCT_1: 13;

    end;

    theorem :: CLOSURE2:35

    g is monotonic & h is monotonic implies (g * h) is monotonic

    proof

      assume that

       A1: g is monotonic and

       A2: h is monotonic;

      

       A3: ( dom h) = ( Bool M) by FUNCT_2:def 1;

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

      assume X c= Y;

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

      then (g . (h . X)) c= (g . (h . Y)) by A1;

      then (g . (h . X)) c= ((g * h) . Y) by A3, FUNCT_1: 13;

      hence thesis by A3, FUNCT_1: 13;

    end;

    theorem :: CLOSURE2:36

    g is idempotent & h is idempotent & (g * h) = (h * g) implies (g * h) is idempotent

    proof

      assume that

       A1: g is idempotent and

       A2: h is idempotent and

       A3: (g * h) = (h * g);

      let X be Element of ( Bool M);

      

       A4: ( dom g) = ( Bool M) by FUNCT_2:def 1;

      

       A5: ( dom h) = ( Bool M) by FUNCT_2:def 1;

      

      hence ((g * h) . X) = (g . (h . X)) by FUNCT_1: 13

      .= (g . (h . (h . X))) by A2

      .= (g . (g . (h . (h . X)))) by A1

      .= (g . ((h * g) . (h . X))) by A3, A5, FUNCT_1: 13

      .= (g . (h . (g . (h . X)))) by A4, FUNCT_1: 13

      .= (g . (h . ((g * h) . X))) by A5, FUNCT_1: 13

      .= ((g * h) . ((g * h) . X)) by A5, FUNCT_1: 13;

    end;

    theorem :: CLOSURE2:37

    g is topological & h is topological implies (g * h) is topological

    proof

      assume that

       A1: g is topological and

       A2: h is topological;

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

      

       A3: ( dom h) = ( Bool M) by FUNCT_2:def 1;

      

      hence ((g * h) . (X (\/) Y)) = (g . (h . (X (\/) Y))) by Th10, FUNCT_1: 13

      .= (g . ((h . X) (\/) (h . Y))) by A2

      .= ((g . (h . X)) (\/) (g . (h . Y))) by A1

      .= (((g * h) . X) (\/) (g . (h . Y))) by A3, FUNCT_1: 13

      .= (((g * h) . X) (\/) ((g * h) . Y)) by A3, FUNCT_1: 13;

    end;

    begin

    reserve S for 1-sorted;

    definition

      let S;

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

the Family -> SubsetFamily of the Sorts #)

       attr strict strict;

    end

    reserve MS for many-sorted over S;

    definition

      let S;

      let IT be ClosureStr over S;

      :: CLOSURE2:def14

      attr IT is additive means

      : Def14: the Family of IT is additive;

      :: CLOSURE2:def15

      attr IT is absolutely-additive means

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

      :: CLOSURE2:def16

      attr IT is multiplicative means

      : Def16: the Family of IT is multiplicative;

      :: CLOSURE2:def17

      attr IT is absolutely-multiplicative means

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

      :: CLOSURE2:def18

      attr IT is properly-upper-bound means

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

      :: CLOSURE2:def19

      attr IT is properly-lower-bound means

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

    end

    definition

      let S, MS;

      :: CLOSURE2:def20

      func Full MS -> ClosureStr over S equals ClosureStr (# the Sorts of MS, ( Bool the Sorts of MS) #);

      correctness ;

    end

    registration

      let S, MS;

      cluster ( Full 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 ( Full 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 ClosureStr over S;

      existence

      proof

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

        take ( Full a);

        thus thesis;

      end;

    end

    registration

      let S;

      let CS be additive ClosureStr over S;

      cluster the Family of CS -> additive;

      coherence by Def14;

    end

    registration

      let S;

      let CS be absolutely-additive ClosureStr over S;

      cluster the Family of CS -> absolutely-additive;

      coherence by Def15;

    end

    registration

      let S;

      let CS be multiplicative ClosureStr over S;

      cluster the Family of CS -> multiplicative;

      coherence by Def16;

    end

    registration

      let S;

      let CS be absolutely-multiplicative ClosureStr over S;

      cluster the Family of CS -> absolutely-multiplicative;

      coherence by Def17;

    end

    registration

      let S;

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

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

      coherence by Def18;

    end

    registration

      let S;

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

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

      coherence by Def19;

    end

    registration

      let S;

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

      let F be SubsetFamily of M;

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

      coherence ;

    end

    registration

      let S, MS;

      let F be additive SubsetFamily of the Sorts of MS;

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

      coherence ;

    end

    registration

      let S, MS;

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

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

      coherence ;

    end

    registration

      let S, MS;

      let F be multiplicative SubsetFamily of the Sorts of MS;

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

      coherence ;

    end

    registration

      let S, MS;

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

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

      coherence ;

    end

    registration

      let S, MS;

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

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

      coherence ;

    end

    registration

      let S, MS;

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

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

      coherence ;

    end

    registration

      let S;

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

      coherence ;

    end

    registration

      let S;

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

      coherence ;

    end

    registration

      let S;

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

      coherence ;

    end

    registration

      let S;

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

      coherence ;

    end

    definition

      let S;

      mode ClosureSystem of S is absolutely-multiplicative ClosureStr over S;

    end

    definition

      let I, M;

      mode ClosureOperator of M is reflexive monotonic idempotent SetOp of M;

    end

    definition

      let S;

      let A be ManySortedSet of the carrier of S;

      let g be ClosureOperator of A;

      :: CLOSURE2:def21

      func ClOp->ClSys g -> strict ClosureStr over S means

      : Def21: the Sorts of it = A & the Family of it = { x where x be Element of ( Bool A) : (g . x) = x };

      existence

      proof

        defpred P[ set] means (g . $1) = $1;

        set SF = { x where x be Element of ( Bool A) : P[x] };

        SF is Subset of ( Bool A) from DOMAIN_1:sch 7;

        then

        reconsider D = SF as SubsetFamily of A;

        take ClosureStr (# A, D #);

        thus thesis;

      end;

      uniqueness ;

    end

    registration

      let S;

      let A be ManySortedSet of the carrier of S;

      let g be ClosureOperator of A;

      cluster ( ClOp->ClSys g) -> absolutely-multiplicative;

      coherence

      proof

        

         A1: the Sorts of ( ClOp->ClSys g) = A by Def21;

        defpred P[ set] means (g . $1) = $1;

        set SF = { x where x be Element of ( Bool A) : P[x] };

        

         A2: SF = the Family of ( ClOp->ClSys g) by Def21;

        SF is Subset of ( Bool A) from DOMAIN_1:sch 7;

        then

        reconsider D = SF as SubsetFamily of A;

        

         A3: ( ClOp->ClSys g) = ClosureStr (# A, D #) by A1, A2;

        D is absolutely-multiplicative

        proof

          let F be SubsetFamily of A such that

           A4: F c= D;

          reconsider mf = ( meet |:F:|) as Element of ( Bool A) by Def1;

          now

            let Z1 be ManySortedSet of the carrier of S;

            assume

             A5: Z1 in F;

            then

            reconsider y1 = Z1 as Element of ( Bool A);

            Z1 in D by A4, A5;

            then

             A6: ex a be Element of ( Bool A) st Z1 = a & (g . a) = a;

            mf c=' y1 by A5, Th21, MSSUBFAM: 43;

            hence (g . mf) c=' Z1 by A6, Def11;

          end;

          then

           A7: (g . mf) c=' mf by Th24;

          mf c=' (g . mf) by Def10;

          then (g . mf) = mf by A7, PBOOLE: 146;

          hence thesis;

        end;

        hence ( ClOp->ClSys g) is absolutely-multiplicative by A3;

      end;

    end

    definition

      let S;

      let A be ClosureSystem of S;

      let C be ManySortedSubset of the Sorts of A;

      :: CLOSURE2:def22

      func Cl C -> Element of ( Bool the Sorts of A) means

      : Def22: ex F be SubsetFamily of the Sorts of A st it = ( meet |:F:|) & F = { X where X be Element of ( Bool the Sorts of A) : C c=' X & X in the Family of A };

      existence

      proof

        defpred P[ Element of ( Bool the Sorts of A)] means C c= $1 & $1 in the Family of A;

        { X where X be Element of ( Bool the Sorts of A) : P[X] } is Subset of ( Bool the Sorts of A) from DOMAIN_1:sch 7;

        then

        reconsider F = { X where X be Element of ( Bool the Sorts of A) : C c= X & X in the Family of A } as SubsetFamily of the Sorts of A;

        reconsider IT = ( meet |:F:|) as Element of ( Bool the Sorts of A) by Def1;

        take IT, F;

        thus thesis;

      end;

      uniqueness ;

    end

    theorem :: CLOSURE2:38

    

     Th38: for D be ClosureSystem of S holds for a be Element of ( Bool the Sorts of D) holds for f be SetOp of the Sorts of D st a in the Family of D & for x be Element of ( Bool the Sorts of D) holds (f . x) = ( Cl x) holds (f . a) = a

    proof

      let D be ClosureSystem of S, a be Element of ( Bool the Sorts of D), f be SetOp of the Sorts of D such that

       A1: a in the Family of D and

       A2: for x be Element of ( Bool the Sorts of D) holds (f . x) = ( Cl x);

      consider F be SubsetFamily of the Sorts of D such that

       A3: ( Cl a) = ( meet |:F:|) and

       A4: F = { X where X be Element of ( Bool the Sorts of D) : a c=' X & X in the Family of D } by Def22;

      

       A5: (f . a) = ( meet |:F:|) by A2, A3;

      a in F by A1, A4;

      then

       A6: (f . a) c= a by A5, Th21, MSSUBFAM: 43;

      for Z1 be ManySortedSet of the carrier of S st Z1 in F holds a c=' Z1

      proof

        let Z1 be ManySortedSet of the carrier of S;

        assume Z1 in F;

        then ex b be Element of ( Bool the Sorts of D) st Z1 = b & a c=' b & b in the Family of D by A4;

        hence thesis;

      end;

      then a c= (f . a) by A5, Th24;

      hence thesis by A6, PBOOLE: 146;

    end;

    theorem :: CLOSURE2:39

    for D be ClosureSystem of S holds for a be Element of ( Bool the Sorts of D) holds for f be SetOp of the Sorts of D st (f . a) = a & for x be Element of ( Bool the Sorts of D) holds (f . x) = ( Cl x) holds a in the Family of D

    proof

      deffunc F( set) = $1;

      let D be ClosureSystem of S, a be Element of ( Bool the Sorts of D), f be SetOp of the Sorts of D such that

       A1: (f . a) = a & for x be Element of ( Bool the Sorts of D) holds (f . x) = ( Cl x);

      set F = the Family of D, M = the Sorts of D;

      defpred P[ Element of ( Bool M)] means a c=' $1;

      defpred R[ Element of ( Bool M)] means a c=' $1 & $1 in F;

      defpred S[ Element of ( Bool M)] means $1 in F & a c=' $1;

      

       A2: { F(w) where w be Element of ( Bool M) : F(w) in F & P[w] } c= F from FRAENKEL:sch 17;

      

       A3: for q be Element of ( Bool M) holds R[q] iff S[q];

      

       A4: { F(s) where s be Element of ( Bool M) : R[s] } = { F(b) where b be Element of ( Bool M) : S[b] } from FRAENKEL:sch 3( A3);

      consider SF be SubsetFamily of M such that

       A5: ( Cl a) = ( meet |:SF:|) and

       A6: SF = { X where X be Element of ( Bool M) : a c= X & X in F } by Def22;

      a = ( meet |:SF:|) by A1, A5;

      hence thesis by A6, A2, A4, Def7;

    end;

    theorem :: CLOSURE2:40

    

     Th40: for D be ClosureSystem of S holds for f be SetOp of the Sorts of D st for x be Element of ( Bool the Sorts of D) holds (f . x) = ( Cl x) holds f is reflexive monotonic idempotent

    proof

      let D be ClosureSystem of S, f be SetOp of the Sorts of D such that

       A1: for x be Element of ( Bool the Sorts of D) holds (f . x) = ( Cl x);

      set M = the Sorts of D;

      

       A2: f is reflexive

      proof

        let x be Element of ( Bool M);

        consider F be SubsetFamily of M such that

         A3: ( Cl x) = ( meet |:F:|) and

         A4: F = { X where X be Element of ( Bool the Sorts of D) : x c=' X & X in the Family of D } by Def22;

        

         A5: for Z1 be ManySortedSet of the carrier of S st Z1 in F holds x c=' Z1

        proof

          let Z1 be ManySortedSet of the carrier of S;

          assume Z1 in F;

          then ex a be Element of ( Bool M) st Z1 = a & x c=' a & a in the Family of D by A4;

          hence thesis;

        end;

        (f . x) = ( meet |:F:|) by A1, A3;

        hence thesis by A5, Th24;

      end;

      

       A6: f is monotonic

      proof

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

         A7: x c=' y;

        consider Fy be SubsetFamily of M such that

         A8: ( Cl y) = ( meet |:Fy:|) and

         A9: Fy = { X where X be Element of ( Bool the Sorts of D) : y c=' X & X in the Family of D } by Def22;

        consider Fx be SubsetFamily of M such that

         A10: ( Cl x) = ( meet |:Fx:|) and

         A11: Fx = { X where X be Element of ( Bool the Sorts of D) : x c=' X & X in the Family of D } by Def22;

         |:Fy:| c=' |:Fx:|

        proof

          let i be object such that

           A12: i in the carrier of S;

          thus ( |:Fy:| . i) c= ( |:Fx:| . i)

          proof

            let q be object such that

             A13: q in ( |:Fy:| . i);

            per cases ;

              suppose Fy is empty;

              then

              reconsider Fy9 = Fy as empty SubsetFamily of M;

              ( |:Fy9:| . i) is empty;

              hence thesis by A13;

            end;

              suppose Fy is non empty;

              then ( |:Fy:| . i) = { (e . i) where e be Element of ( Bool M) : e in Fy } by A12, Th14;

              then

              consider w be Element of ( Bool M) such that

               A14: q = (w . i) and

               A15: w in Fy by A13;

              

               A16: ex r be Element of ( Bool M) st r = w & y c=' r & r in the Family of D by A9, A15;

              then x c=' w by A7, PBOOLE: 13;

              then

               A17: w in Fx by A11, A16;

              then ( |:Fx:| . i) = { (e . i) where e be Element of ( Bool M) : e in Fx } by A12, Th14;

              hence thesis by A14, A17;

            end;

          end;

        end;

        then ( meet |:Fx:|) c=' ( meet |:Fy:|) by MSSUBFAM: 46;

        then ( meet |:Fx:|) c=' (f . y) by A1, A8;

        hence thesis by A1, A10;

      end;

      f is idempotent

      proof

        let x be Element of ( Bool M);

        consider F be SubsetFamily of M such that

         A18: ( Cl x) = ( meet |:F:|) and

         A19: F = { X where X be Element of ( Bool the Sorts of D) : x c=' X & X in the Family of D } by Def22;

        F c= the Family of D

        proof

          let k be object;

          assume k in F;

          then ex q be Element of ( Bool M) st k = q & x c=' q & q in the Family of D by A19;

          hence thesis;

        end;

        then

         A20: ( meet |:F:|) in the Family of D by Def7;

        

        thus (f . x) = ( meet |:F:|) by A1, A18

        .= (f . ( meet |:F:|)) by A1, A20, Th38

        .= (f . (f . x)) by A1, A18;

      end;

      hence thesis by A2, A6;

    end;

    definition

      let S;

      let D be ClosureSystem of S;

      :: CLOSURE2:def23

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

      : Def23: for x be Element of ( Bool the Sorts of D) holds (it . x) = ( Cl x);

      existence

      proof

        set M = the Sorts of D;

        deffunc F( Element of ( Bool M)) = ( Cl $1);

        consider f be Function of ( Bool M), ( Bool M) such that

         A1: for x be Element of ( Bool M) holds (f . x) = F(x) from FUNCT_2:sch 4;

        reconsider f as SetOp of M;

        reconsider f as ClosureOperator of M by A1, Th40;

        take f;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let f,g be ClosureOperator of the Sorts of D such that

         A2: for x be Element of ( Bool the Sorts of D) holds (f . x) = ( Cl x) and

         A3: for x be Element of ( Bool the Sorts of D) holds (g . x) = ( Cl x);

        now

          set X = ( Bool the Sorts of D);

          thus X = ( dom f) by FUNCT_2:def 1;

          thus X = ( dom g) by FUNCT_2:def 1;

          let x be object;

          assume x in X;

          then

          reconsider x1 = x as Element of ( Bool the Sorts of D);

          

          thus (f . x) = ( Cl x1) by A2

          .= (g . x) by A3;

        end;

        hence f = g;

      end;

    end

    theorem :: CLOSURE2:41

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

    proof

      let A be ManySortedSet of the carrier of S, f be ClosureOperator of A;

      set D = ( ClOp->ClSys f), M = the Sorts of D, f1 = ( ClSys->ClOp D);

      

       A1: A = M by Def21;

      then

      reconsider ff = f as reflexive idempotent monotonic SetOp of M;

      for x be object st x in ( Bool A) holds (f1 . x) = (ff . x)

      proof

        let x be object;

        assume x in ( Bool A);

        then

        reconsider x1 = x as Element of ( Bool M) by Def21;

        consider F be SubsetFamily of M such that

         A2: ( Cl x1) = ( meet |:F:|) and

         A3: F = { X where X be Element of ( Bool M) : x1 c=' X & X in the Family of D } by Def22;

         A4:

        now

          

           A5: x1 c=' (ff . x1) by Def10;

          x1 c=' M & M in the Family of D by Def8, PBOOLE:def 18;

          then M in F by A3;

          then

          reconsider F9 = F as non empty SubsetFamily of M;

          let i be object;

          assume

           A6: i in the carrier of S;

          then

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

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

           A8: (( meet |:F:|) . i) = ( Intersect Q) by MSSUBFAM:def 1;

          

           A9: Q = { (q . i) where q be Element of ( Bool M) : q in F9 } by A6, A7, Th14;

          

           A10: the Family of D = { q where q be Element of ( Bool M) : (ff . q) = q } by A1, Def21;

           A11:

          now

            let z be set;

            assume z in Q;

            then

            consider q be Element of ( Bool M) such that

             A12: z = (q . i) and

             A13: q in F9 by A9;

            consider X be Element of ( Bool M) such that

             A14: q = X and

             A15: x1 c=' X & X in the Family of D by A3, A13;

            (ex t be Element of ( Bool M) st X = t & (ff . t) = t) & (ff . x1) c=' (ff . X) by A10, A15, Def11;

            hence ((ff . x1) . i) c= z by A6, A12, A14;

          end;

          (ff . (ff . x1)) = (ff . x1) by Def12;

          then (ff . x1) in the Family of D by A10;

          then (ff . x1) in F9 by A3, A5;

          then ((ff . x1) . i) in Q by A9;

          then

           A16: (( meet |:F:|) . i) c= ((ff . x1) . i) by A8, MSSUBFAM: 2;

          Q = ( |:F9:| . i) by A7;

          then ((ff . x1) . i) c= (( meet |:F:|) . i) by A6, A8, A11, MSSUBFAM: 5;

          hence (( meet |:F:|) . i) = ((ff . x1) . i) by A16;

        end;

        

        thus (f1 . x) = ( Cl x1) by Def23

        .= (ff . x) by A2, A4, PBOOLE: 3;

      end;

      hence thesis by A1, FUNCT_2: 12;

    end;

    deffunc F( set) = $1;

    theorem :: CLOSURE2:42

    for D be ClosureSystem of S holds ( ClOp->ClSys ( ClSys->ClOp D)) = the ClosureStr of D

    proof

      let D be ClosureSystem of S;

      set M = the Sorts of D, F = the Family of D, d = the Family of ( ClOp->ClSys ( ClSys->ClOp D)), f = ( ClSys->ClOp D);

      

       A1: d = { x where x be Element of ( Bool M) : (f . x) = x } by Def21;

      F = d

      proof

        thus F c= d

        proof

          let q be object;

          assume

           A2: q in F;

          then

          reconsider q1 = q as Element of ( Bool M);

          consider SF be SubsetFamily of M such that

           A3: ( Cl q1) = ( meet |:SF:|) and

           A4: SF = { X where X be Element of ( Bool M) : q1 c= X & X in F } by Def22;

          q1 c=' M & M in F by Def8, PBOOLE:def 18;

          then M in SF by A4;

          then

          reconsider SF9 = SF as non empty SubsetFamily of M;

          now

            let i be object;

            assume

             A5: i in the carrier of S;

            then

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

             A6: Q = ( |:SF9:| . i) and

             A7: (( meet |:SF9:|) . i) = ( Intersect Q) by MSSUBFAM:def 1;

            

             A8: Q = { (x . i) where x be Element of ( Bool M) : x in SF9 } by A5, A6, Th14;

            q1 in SF9 by A2, A4;

            then

             A9: (q1 . i) in Q by A8;

            then

             A10: ( Intersect Q) c= (q1 . i) by MSSUBFAM: 2;

            now

              let z be set;

              assume z in Q;

              then

              consider x be Element of ( Bool M) such that

               A11: z = (x . i) and

               A12: x in SF9 by A8;

              ex xx be Element of ( Bool M) st xx = x & q1 c=' xx & xx in F by A4, A12;

              hence (q1 . i) c= z by A5, A11;

            end;

            then (q1 . i) c= ( Intersect Q) by A9, MSSUBFAM: 5;

            then ( Intersect Q) = (q1 . i) by A10;

            hence ((f . q1) . i) = (q1 . i) by A3, A7, Def23;

          end;

          then (f . q1) = q1;

          hence thesis by A1;

        end;

        let q be object;

        assume q in d;

        then

        consider x be Element of ( Bool M) such that

         A13: q = x & (f . x) = x by A1;

        defpred S[ Element of ( Bool M)] means $1 in F & x c=' $1;

        defpred R[ Element of ( Bool M)] means x c=' $1 & $1 in F;

        defpred P[ Element of ( Bool M)] means x c=' $1;

        

         A14: { F(w) where w be Element of ( Bool M) : F(w) in F & P[w] } c= F from FRAENKEL:sch 17;

        

         A15: for a be Element of ( Bool M) holds R[a] iff S[a];

        

         A16: { F(a) where a be Element of ( Bool M) : R[a] } = { F(b) where b be Element of ( Bool M) : S[b] } from FRAENKEL:sch 3( A15);

        consider SF be SubsetFamily of M such that

         A17: ( Cl x) = ( meet |:SF:|) and

         A18: SF = { X where X be Element of ( Bool M) : x c=' X & X in F } by Def22;

        ( meet |:SF:|) = q by A13, A17, Def23;

        hence thesis by A18, A14, A16, Def7;

      end;

      hence thesis by Def21;

    end;