mssubfam.miz



    begin

    registration

      let I be set;

      let F be ManySortedFunction of I;

      cluster ( doms F) -> I -defined;

      coherence

      proof

        ( dom ( doms F)) = ( dom F) by FUNCT_6: 59

        .= I by PARTFUN1:def 2;

        hence thesis by RELAT_1:def 18;

      end;

      cluster ( rngs F) -> I -defined;

      coherence

      proof

        ( dom ( rngs F)) = ( dom F) by FUNCT_6: 60

        .= I by PARTFUN1:def 2;

        hence thesis by RELAT_1:def 18;

      end;

    end

    registration

      let I be set;

      let F be ManySortedFunction of I;

      cluster ( doms F) -> total;

      coherence

      proof

        ( dom ( doms F)) = ( dom F) by FUNCT_6: 59

        .= I by PARTFUN1:def 2;

        hence thesis by PARTFUN1:def 2;

      end;

      cluster ( rngs F) -> total;

      coherence

      proof

        ( dom ( rngs F)) = ( dom F) by FUNCT_6: 60

        .= I by PARTFUN1:def 2;

        hence thesis by PARTFUN1:def 2;

      end;

    end

    reserve I,G,H for set,

i,x for object,

A,B,M for ManySortedSet of I,

sf,sg,sh for Subset-Family of I,

v,w for Subset of I,

F for ManySortedFunction of I;

    scheme :: MSSUBFAM:sch1

    MSFExFunc { I() -> set , A,B() -> ManySortedSet of I() , P[ object, object, object] } :

ex F be ManySortedFunction of A(), B() st for i be object st i in I() holds ex f be Function of (A() . i), (B() . i) st f = (F . i) & for x be object st x in (A() . i) holds P[(f . x), x, i]

      provided

       A1: for i be object st i in I() holds for x be object st x in (A() . i) holds ex y be object st y in (B() . i) & P[y, x, i];

      defpred Q[ object, object] means ex f1 be Function of (A() . $1), (B() . $1) st f1 = $2 & for x be object st x in (A() . $1) holds P[(f1 . x), x, $1];

       A2:

      now

        let i be object such that

         A3: i in I();

        per cases ;

          suppose (B() . i) is non empty;

          then

          reconsider bb = (B() . i) as non empty set;

          defpred Z[ object, object] means P[$2, $1, i];

          

           A4: for e be object st e in (A() . i) holds ex u be object st u in bb & Z[e, u] by A1, A3;

          consider ff be Function of (A() . i), bb such that

           A5: for e be object st e in (A() . i) holds Z[e, (ff . e)] from FUNCT_2:sch 1( A4);

          reconsider fff = ff as Function of (A() . i), (B() . i);

          reconsider j = fff as object;

          take j;

          thus Q[i, j] by A5;

        end;

          suppose

           A6: (B() . i) is empty;

           A7:

          now

            let x be object;

            for y be object holds not (y in (B() . i) & P[y, x, i]) by A6;

            hence not x in (A() . i) by A1, A3;

          end;

          then (A() . i) = {} by XBOOLE_0:def 1;

          then

          reconsider fff = {} as Function of (A() . i), (B() . i) by RELSET_1: 12;

          reconsider j = fff as object;

          take j;

          thus Q[i, j]

          proof

            take fff;

            thus fff = j;

            thus thesis by A7;

          end;

        end;

      end;

      consider F be ManySortedSet of I() such that

       A8: for i be object st i in I() holds Q[i, (F . i)] from PBOOLE:sch 3( A2);

      F is ManySortedFunction of A(), B()

      proof

        let i be object;

        assume i in I();

        then ex f be Function of (A() . i), (B() . i) st f = (F . i) & for x be object st x in (A() . i) holds P[(f . x), x, i] by A8;

        hence thesis;

      end;

      then

      reconsider F as ManySortedFunction of A(), B();

      take F;

      thus thesis by A8;

    end;

    theorem :: MSSUBFAM:1

    sf <> {} implies ( Intersect sf) c= ( union sf)

    proof

      assume sf <> {} ;

      then ( Intersect sf) = ( meet sf) by SETFAM_1:def 9;

      hence thesis by SETFAM_1: 2;

    end;

    theorem :: MSSUBFAM:2

    G in sf implies ( Intersect sf) c= G

    proof

      assume

       A1: G in sf;

      then ( meet sf) = ( Intersect sf) by SETFAM_1:def 9;

      hence thesis by A1, SETFAM_1: 3;

    end;

    theorem :: MSSUBFAM:3

     {} in sf implies ( Intersect sf) = {}

    proof

      assume

       A1: {} in sf;

      then ( Intersect sf) = ( meet sf) by SETFAM_1:def 9;

      hence thesis by A1, SETFAM_1: 4;

    end;

    theorem :: MSSUBFAM:4

    for Z be Subset of I holds (for Z1 be set st Z1 in sf holds Z c= Z1) implies Z c= ( Intersect sf)

    proof

      let Z be Subset of I such that

       A1: for Z1 be set st Z1 in sf holds Z c= Z1;

      per cases ;

        suppose

         A2: sf <> {} ;

        then ( Intersect sf) = ( meet sf) by SETFAM_1:def 9;

        hence thesis by A1, A2, SETFAM_1: 5;

      end;

        suppose sf = {} ;

        then ( Intersect sf) = I by SETFAM_1:def 9;

        hence thesis;

      end;

    end;

    theorem :: MSSUBFAM:5

    sf <> {} & (for Z1 be set st Z1 in sf holds G c= Z1) implies G c= ( Intersect sf)

    proof

      assume that

       A1: sf <> {} and

       A2: for Z1 be set st Z1 in sf holds G c= Z1;

      ( Intersect sf) = ( meet sf) by A1, SETFAM_1:def 9;

      hence thesis by A1, A2, SETFAM_1: 5;

    end;

    theorem :: MSSUBFAM:6

    G in sf & G c= H implies ( Intersect sf) c= H

    proof

      assume that

       A1: G in sf and

       A2: G c= H;

      ( Intersect sf) = ( meet sf) by A1, SETFAM_1:def 9;

      hence thesis by A1, A2, SETFAM_1: 7;

    end;

    theorem :: MSSUBFAM:7

    G in sf & G misses H implies ( Intersect sf) misses H

    proof

      assume that

       A1: G in sf and

       A2: G misses H;

      ( Intersect sf) = ( meet sf) by A1, SETFAM_1:def 9;

      hence thesis by A1, A2, SETFAM_1: 8;

    end;

    theorem :: MSSUBFAM:8

    sh = (sf \/ sg) implies ( Intersect sh) = (( Intersect sf) /\ ( Intersect sg))

    proof

      assume

       A1: sh = (sf \/ sg);

      per cases ;

        suppose sf = {} & sg = {} ;

        hence thesis by A1;

      end;

        suppose

         A2: sf <> {} & sg = {} ;

        

        hence ( Intersect sh) = ( meet sf) by A1, SETFAM_1:def 9

        .= (( meet sf) /\ I) by XBOOLE_1: 28

        .= (( Intersect sf) /\ I) by A2, SETFAM_1:def 9

        .= (( Intersect sf) /\ ( Intersect sg)) by A2, SETFAM_1:def 9;

      end;

        suppose

         A3: sf = {} & sg <> {} ;

        

        hence ( Intersect sh) = ( meet sg) by A1, SETFAM_1:def 9

        .= (I /\ ( meet sg)) by XBOOLE_1: 28

        .= (I /\ ( Intersect sg)) by A3, SETFAM_1:def 9

        .= (( Intersect sf) /\ ( Intersect sg)) by A3, SETFAM_1:def 9;

      end;

        suppose

         A4: sf <> {} & sg <> {} ;

        then

         A5: ( Intersect sg) = ( meet sg) by SETFAM_1:def 9;

        ( Intersect sh) = ( meet sh) & ( Intersect sf) = ( meet sf) by A1, A4, SETFAM_1:def 9;

        hence thesis by A1, A4, A5, SETFAM_1: 9;

      end;

    end;

    theorem :: MSSUBFAM:9

    sf = {v} implies ( Intersect sf) = v

    proof

      assume

       A1: sf = {v};

      then ( Intersect sf) = ( meet sf) by SETFAM_1:def 9;

      hence thesis by A1, SETFAM_1: 10;

    end;

    theorem :: MSSUBFAM:10

    sf = {v, w} implies ( Intersect sf) = (v /\ w)

    proof

      assume

       A1: sf = {v, w};

      then ( Intersect sf) = ( meet sf) by SETFAM_1:def 9;

      hence thesis by A1, SETFAM_1: 11;

    end;

    theorem :: MSSUBFAM:11

    A in B implies A is Element of B

    proof

      assume

       A1: A in B;

      let i be object;

      assume i in I;

      hence thesis by A1;

    end;

    theorem :: MSSUBFAM:12

    for B be non-empty ManySortedSet of I holds A is Element of B implies A in B

    proof

      let B be non-empty ManySortedSet of I;

      assume

       A1: A is Element of B;

      let i be object;

      assume

       A2: i in I;

      then

       A3: (B . i) <> {} ;

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

      hence thesis by A3;

    end;

    theorem :: MSSUBFAM:13

    

     Th13: for f be Function st i in I & f = (F . i) holds (( rngs F) . i) = ( rng f)

    proof

      

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

      let f be Function;

      assume i in I & f = (F . i);

      hence thesis by A1, FUNCT_6: 22;

    end;

    theorem :: MSSUBFAM:14

    

     Th14: for f be Function st i in I & f = (F . i) holds (( doms F) . i) = ( dom f)

    proof

      

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

      let f be Function;

      assume i in I & f = (F . i);

      hence thesis by A1, FUNCT_6: 22;

    end;

    theorem :: MSSUBFAM:15

    for F,G be ManySortedFunction of I holds (G ** F) is ManySortedFunction of I

    proof

      let F,G be ManySortedFunction of I;

      ( dom (G ** F)) = (( dom F) /\ ( dom G)) by PBOOLE:def 19

      .= (I /\ ( dom G)) by PARTFUN1:def 2

      .= (I /\ I) by PARTFUN1:def 2

      .= I;

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

    end;

    theorem :: MSSUBFAM:16

    for A be non-empty ManySortedSet of I holds for F be ManySortedFunction of A, ( EmptyMS I) holds F = ( EmptyMS I)

    proof

      let A be non-empty ManySortedSet of I;

      let F be ManySortedFunction of A, ( EmptyMS I);

      now

        let i be object;

        assume i in I;

        then

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

        f = {} ;

        hence (F . i) = (( EmptyMS I) . i);

      end;

      hence thesis;

    end;

    theorem :: MSSUBFAM:17

    A is_transformable_to B & F is ManySortedFunction of A, B implies ( doms F) = A & ( rngs F) c= B

    proof

      assume that

       A1: A is_transformable_to B and

       A2: F is ManySortedFunction of A, B;

      now

        let i be object;

        assume

         A3: i in I;

        then

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

        

         A4: (B . i) = {} implies (A . i) = {} by A1, A3, PZFMISC1:def 3;

        

        thus (( doms F) . i) = ( dom f) by A3, Th14

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

      end;

      hence ( doms F) = A;

      let i be object;

      assume

       A5: i in I;

      then

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

      ( rng f) c= (B . i) by RELAT_1:def 19;

      hence thesis by A5, Th13;

    end;

    begin

    registration

      let I;

      cluster empty-yielding -> finite-yielding for ManySortedSet of I;

      coherence

      proof

        let A be ManySortedSet of I such that

         A1: A is empty-yielding;

        let i be object;

        assume i in I;

        reconsider B = (A . i) as empty set by A1;

        B is finite;

        hence thesis;

      end;

    end

    registration

      let I;

      cluster ( EmptyMS I) -> empty-yielding finite-yielding;

      coherence ;

    end

    registration

      let I, A;

      cluster empty-yielding finite-yielding for ManySortedSubset of A;

      existence

      proof

        set x = ( EmptyMS I);

        x c= A by PBOOLE: 43;

        then

        reconsider x as ManySortedSubset of A by PBOOLE:def 18;

        take x;

        thus thesis;

      end;

    end

    theorem :: MSSUBFAM:18

    

     Th18: A c= B & B is finite-yielding implies A is finite-yielding

    proof

      assume

       A1: A c= B & B is finite-yielding;

      let i be object;

      assume i in I;

      then (A . i) c= (B . i) & (B . i) is finite by A1;

      hence thesis;

    end;

    registration

      let I;

      let A be finite-yielding ManySortedSet of I;

      cluster -> finite-yielding for ManySortedSubset of A;

      coherence by PBOOLE:def 18, Th18;

    end

    registration

      let I;

      let A,B be finite-yielding ManySortedSet of I;

      cluster (A (\/) B) -> finite-yielding;

      coherence

      proof

        let i be object;

        assume

         A1: i in I;

        ((A . i) \/ (B . i)) is finite;

        hence thesis by A1, PBOOLE:def 4;

      end;

    end

    registration

      let I, A;

      let B be finite-yielding ManySortedSet of I;

      cluster (A (/\) B) -> finite-yielding;

      coherence

      proof

        let i be object;

        assume

         A1: i in I;

        ((A . i) /\ (B . i)) is finite;

        hence thesis by A1, PBOOLE:def 5;

      end;

    end

    registration

      let I, B;

      let A be finite-yielding ManySortedSet of I;

      cluster (A (/\) B) -> finite-yielding;

      coherence ;

    end

    registration

      let I, B;

      let A be finite-yielding ManySortedSet of I;

      cluster (A (\) B) -> finite-yielding;

      coherence

      proof

        let i be object;

        assume

         A1: i in I;

        ((A . i) \ (B . i)) is finite;

        hence thesis by A1, PBOOLE:def 6;

      end;

    end

    registration

      let I, F;

      let A be finite-yielding ManySortedSet of I;

      cluster (F .:.: A) -> finite-yielding;

      coherence

      proof

        let i be object such that

         A1: i in I;

        reconsider f = (F . i) as Function;

        (f .: (A . i)) is finite;

        hence thesis by A1, PBOOLE:def 20;

      end;

    end

    registration

      let I;

      let A,B be finite-yielding ManySortedSet of I;

      cluster [|A, B|] -> finite-yielding;

      coherence

      proof

        let i be object;

        assume

         A1: i in I;

         [:(A . i), (B . i):] is finite;

        hence thesis by A1, PBOOLE:def 16;

      end;

    end

    theorem :: MSSUBFAM:19

    B is non-empty & [|A, B|] is finite-yielding implies A is finite-yielding

    proof

      assume that

       A1: B is non-empty and

       A2: [|A, B|] is finite-yielding;

      let i be object;

      assume

       A3: i in I;

      ( [|A, B|] . i) is finite by A2;

      then [:(A . i), (B . i):] is finite by A3, PBOOLE:def 16;

      hence thesis by A1, A3;

    end;

    theorem :: MSSUBFAM:20

    A is non-empty & [|A, B|] is finite-yielding implies B is finite-yielding

    proof

      assume that

       A1: A is non-empty and

       A2: [|A, B|] is finite-yielding;

      let i be object;

      assume

       A3: i in I;

      ( [|A, B|] . i) is finite by A2;

      then [:(A . i), (B . i):] is finite by A3, PBOOLE:def 16;

      hence thesis by A1, A3;

    end;

    theorem :: MSSUBFAM:21

    

     Th21: A is finite-yielding iff ( bool A) is finite-yielding

    proof

      thus A is finite-yielding implies ( bool A) is finite-yielding

      proof

        assume

         A1: A is finite-yielding;

        let i be object;

        assume

         A2: i in I;

        (A . i) is finite by A1;

        then ( bool (A . i)) is finite;

        hence thesis by A2, MBOOLEAN:def 1;

      end;

      assume

       A3: ( bool A) is finite-yielding;

      let i be object;

      assume

       A4: i in I;

      (( bool A) . i) is finite by A3;

      then ( bool (A . i)) is finite by A4, MBOOLEAN:def 1;

      hence thesis;

    end;

    registration

      let I;

      let M be finite-yielding ManySortedSet of I;

      cluster ( bool M) -> finite-yielding;

      coherence by Th21;

    end

    theorem :: MSSUBFAM:22

    for A be non-empty ManySortedSet of I holds A is finite-yielding & (for M be ManySortedSet of I st M in A holds M is finite-yielding) implies ( union A) is finite-yielding

    proof

      let A be non-empty ManySortedSet of I;

      assume that

       A1: A is finite-yielding and

       A2: for M be ManySortedSet of I st M in A holds M is finite-yielding;

      let i be object;

      assume

       A3: i in I;

      

       A4: for X9 be set st X9 in (A . i) holds X9 is finite

      proof

        consider M be ManySortedSet of I such that

         A5: M in A by PBOOLE: 134;

        let X9 be set such that

         A6: X9 in (A . i);

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

        then

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

        

         A7: ( dom (i .--> X9)) = {i};

        i in {i} by TARSKI:def 1;

        

        then

         A8: (K . i) = ((i .--> X9) . i) by A7, FUNCT_4: 13

        .= X9 by FUNCOP_1: 72;

        K in A

        proof

          let j be object such that

           A9: j in I;

          now

            per cases ;

              case j = i;

              hence thesis by A6, A8;

            end;

              case j <> i;

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

              then (K . j) = (M . j) by FUNCT_4: 11;

              hence thesis by A5, A9;

            end;

          end;

          hence thesis;

        end;

        then K is finite-yielding by A2;

        hence thesis by A8;

      end;

      (A . i) is finite by A1;

      then ( union (A . i)) is finite by A4, FINSET_1: 7;

      hence thesis by A3, MBOOLEAN:def 2;

    end;

    theorem :: MSSUBFAM:23

    ( union A) is finite-yielding implies A is finite-yielding & for M st M in A holds M is finite-yielding

    proof

      assume

       A1: ( union A) is finite-yielding;

      thus A is finite-yielding

      proof

        let i be object;

        assume

         A2: i in I;

        (( union A) . i) is finite by A1;

        then ( union (A . i)) is finite by A2, MBOOLEAN:def 2;

        hence thesis by FINSET_1: 7;

      end;

      let M such that

       A3: M in A;

      let i be object;

      assume

       A4: i in I;

      (( union A) . i) is finite by A1;

      then

       A5: ( union (A . i)) is finite by A4, MBOOLEAN:def 2;

      (M . i) in (A . i) by A3, A4;

      hence thesis by A5, FINSET_1: 7;

    end;

    theorem :: MSSUBFAM:24

    ( doms F) is finite-yielding implies ( rngs F) is finite-yielding

    proof

      assume

       A1: ( doms F) is finite-yielding;

      let i be object such that

       A2: i in I;

      reconsider f = (F . i) as Function;

      (( doms F) . i) is finite by A1;

      then ( dom f) is finite by A2, Th14;

      then ( rng f) is finite by FINSET_1: 8;

      hence thesis by A2, Th13;

    end;

    theorem :: MSSUBFAM:25

    (A c= ( rngs F) & for i be set holds for f be Function st i in I & f = (F . i) holds (f " (A . i)) is finite) implies A is finite-yielding

    proof

      assume that

       A1: A c= ( rngs F) and

       A2: for i be set holds for f be Function st i in I & f = (F . i) holds (f " (A . i)) is finite;

      let i such that

       A3: i in I;

      reconsider f = (F . i) as Function;

      (( rngs F) . i) = ( rng f) by A3, Th13;

      then

       A4: (A . i) c= ( rng f) by A1, A3;

      (f " (A . i)) is finite by A2, A3;

      hence thesis by A4, FINSET_1: 9;

    end;

    registration

      let I;

      let A,B be finite-yielding ManySortedSet of I;

      cluster ( (Funcs) (A,B)) -> finite-yielding;

      coherence

      proof

        let i be object;

        assume i in I;

        then (( (Funcs) (A,B)) . i) = ( Funcs ((A . i),(B . i))) & (A . i) is finite by PBOOLE:def 17;

        hence thesis by FRAENKEL: 6;

      end;

    end

    registration

      let I;

      let A,B be finite-yielding ManySortedSet of I;

      cluster (A (\+\) B) -> finite-yielding;

      coherence ;

    end

    reserve X,Y,Z for ManySortedSet of I;

    theorem :: MSSUBFAM:26

    X is finite-yielding & X c= [|Y, Z|] implies ex A, B st A is finite-yielding & A c= Y & B is finite-yielding & B c= Z & X c= [|A, B|]

    proof

      assume that

       A1: X is finite-yielding and

       A2: X c= [|Y, Z|];

      defpred Q[ object, object] means ex D,b be set st D = $2 & D is finite & D c= (Y . $1) & b is finite & b c= (Z . $1) & (X . $1) c= [:D, b:];

      

       A3: for i be object st i in I holds ex j be object st Q[i, j]

      proof

        let i be object;

        assume

         A4: i in I;

        then (X . i) c= ( [|Y, Z|] . i) by A2;

        then

         A5: (X . i) c= [:(Y . i), (Z . i):] by A4, PBOOLE:def 16;

        (X . i) is finite by A1;

        then

        consider A,B be set such that

         A6: A is finite & A c= (Y . i) & B is finite & B c= (Z . i) & (X . i) c= [:A, B:] by A5, FINSET_1: 13;

        thus thesis by A6;

      end;

      consider A be ManySortedSet of I such that

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

      defpred P[ object, object] means ex D be set st D = $2 & (A . $1) is finite & (A . $1) c= (Y . $1) & D is finite & D c= (Z . $1) & (X . $1) c= [:(A . $1), D:];

      

       A8: for i be object st i in I holds ex j be object st P[i, j]

      proof

        let i be object;

        assume i in I;

        then Q[i, (A . i)] by A7;

        hence thesis;

      end;

      consider B be ManySortedSet of I such that

       A9: for i be object st i in I holds P[i, (B . i)] from PBOOLE:sch 3( A8);

      take A, B;

      thus A is finite-yielding

      proof

        let i be object;

        assume i in I;

        then P[i, (B . i)] by A9;

        hence thesis;

      end;

      thus A c= Y

      proof

        let i be object;

        assume i in I;

        then P[i, (B . i)] by A9;

        hence thesis;

      end;

      thus B is finite-yielding

      proof

        let i be object;

        assume i in I;

        then P[i, (B . i)] by A9;

        hence thesis;

      end;

      thus B c= Z

      proof

        let i be object;

        assume i in I;

        then P[i, (B . i)] by A9;

        hence thesis;

      end;

      thus X c= [|A, B|]

      proof

        let i be object;

        assume

         A10: i in I;

        then P[i, (B . i)] by A9;

        then (X . i) c= [:(A . i), (B . i):];

        hence thesis by A10, PBOOLE:def 16;

      end;

    end;

    theorem :: MSSUBFAM:27

    X is finite-yielding & X c= [|Y, Z|] implies ex A st A is finite-yielding & A c= Y & X c= [|A, Z|]

    proof

      assume that

       A1: X is finite-yielding and

       A2: X c= [|Y, Z|];

      defpred P[ object, object] means ex D be set st D = $2 & D is finite & D c= (Y . $1) & (X . $1) c= [:D, (Z . $1):];

      

       A3: for i be object st i in I holds ex j be object st P[i, j]

      proof

        let i be object;

        assume

         A4: i in I;

        then (X . i) c= ( [|Y, Z|] . i) by A2;

        then

         A5: (X . i) c= [:(Y . i), (Z . i):] by A4, PBOOLE:def 16;

        (X . i) is finite by A1;

        then

        consider A9 be set such that

         A6: A9 is finite & A9 c= (Y . i) & (X . i) c= [:A9, (Z . i):] by A5, FINSET_1: 14;

        take A9;

        thus thesis by A6;

      end;

      consider A such that

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

      take A;

      thus A is finite-yielding

      proof

        let i be object;

        assume i in I;

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

        hence thesis;

      end;

      thus A c= Y

      proof

        let i be object;

        assume i in I;

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

        hence thesis;

      end;

      thus X c= [|A, Z|]

      proof

        let i be object;

        assume

         A8: i in I;

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

        then (X . i) c= [:(A . i), (Z . i):];

        hence thesis by A8, PBOOLE:def 16;

      end;

    end;

    theorem :: MSSUBFAM:28

    for M be non-empty finite-yielding ManySortedSet of I st for A,B be ManySortedSet of I st A in M & B in M holds A c= B or B c= A holds ex m be ManySortedSet of I st m in M & for K be ManySortedSet of I st K in M holds m c= K

    proof

      let M be non-empty finite-yielding ManySortedSet of I such that

       A1: for A,B be ManySortedSet of I st A in M & B in M holds A c= B or B c= A;

      defpred Q[ object, object] means ex D be set st D = $2 & $2 in (M . $1) & for D9 be set st D9 in (M . $1) holds D c= D9;

      

       A2: for i be object st i in I holds ex j be object st Q[i, j]

      proof

        let i be object;

        assume

         A3: i in I;

        (M . i) is c=-linear

        proof

          consider c9 be ManySortedSet of I such that

           A4: c9 in M by PBOOLE: 134;

          consider b9 be ManySortedSet of I such that

           A5: b9 in M by PBOOLE: 134;

          let B9,C9 be set such that

           A6: B9 in (M . i) and

           A7: C9 in (M . i);

          

           A8: ( dom (i .--> B9)) = {i};

          set qc = (c9 +* (i .--> C9));

          ( dom qc) = I by A3, PZFMISC1: 1;

          then

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

          

           A9: ( dom (i .--> C9)) = {i};

          i in {i} by TARSKI:def 1;

          

          then

           A10: (qc . i) = ((i .--> C9) . i) by A9, FUNCT_4: 13

          .= C9 by FUNCOP_1: 72;

          

           A11: qc in M

          proof

            let j be object such that

             A12: j in I;

            now

              per cases ;

                case j = i;

                hence thesis by A7, A10;

              end;

                case j <> i;

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

                then (qc . j) = (c9 . j) by FUNCT_4: 11;

                hence thesis by A4, A12;

              end;

            end;

            hence thesis;

          end;

          set qb = (b9 +* (i .--> B9));

          ( dom qb) = I by A3, PZFMISC1: 1;

          then

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

          assume

           A13: not B9 c= C9;

          i in {i} by TARSKI:def 1;

          

          then

           A14: (qb . i) = ((i .--> B9) . i) by A8, FUNCT_4: 13

          .= B9 by FUNCOP_1: 72;

          qb in M

          proof

            let j be object such that

             A15: j in I;

            now

              per cases ;

                case j = i;

                hence thesis by A6, A14;

              end;

                case j <> i;

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

                then (qb . j) = (b9 . j) by FUNCT_4: 11;

                hence thesis by A5, A15;

              end;

            end;

            hence thesis;

          end;

          then qb c= qc or qc c= qb by A1, A11;

          hence thesis by A3, A13, A14, A10;

        end;

        then

        consider m9 be set such that

         A16: m9 in (M . i) & for D9 be set st D9 in (M . i) holds m9 c= D9 by A3, FINSET_1: 11;

        take m9;

        thus thesis by A16;

      end;

      consider m be ManySortedSet of I such that

       A17: for i be object st i in I holds Q[i, (m . i)] from PBOOLE:sch 3( A2);

      take m;

      thus m in M

      proof

        let i be object;

        assume i in I;

        then Q[i, (m . i)] by A17;

        hence thesis;

      end;

      thus for C be ManySortedSet of I st C in M holds m c= C

      proof

        let C be ManySortedSet of I such that

         A18: C in M;

        let i be object;

        assume

         A19: i in I;

        then

         A20: (C . i) in (M . i) by A18;

         Q[i, (m . i)] by A17, A19;

        hence thesis by A20;

      end;

    end;

    theorem :: MSSUBFAM:29

    for M be non-empty finite-yielding ManySortedSet of I st for A,B be ManySortedSet of I st A in M & B in M holds A c= B or B c= A holds ex m be ManySortedSet of I st m in M & for K be ManySortedSet of I st K in M holds K c= m

    proof

      let M be non-empty finite-yielding ManySortedSet of I such that

       A1: for A,B be ManySortedSet of I st A in M & B in M holds A c= B or B c= A;

      defpred Z[ object, object] means ex X be set st X = $2 & $2 in (M . $1) & for D9 be set st D9 in (M . $1) holds D9 c= X;

      

       A2: for i be object st i in I holds ex j be object st Z[i, j]

      proof

        let i be object;

        assume

         A3: i in I;

        (M . i) is c=-linear

        proof

          consider c9 be ManySortedSet of I such that

           A4: c9 in M by PBOOLE: 134;

          consider b9 be ManySortedSet of I such that

           A5: b9 in M by PBOOLE: 134;

          let B9,C9 be set such that

           A6: B9 in (M . i) and

           A7: C9 in (M . i);

          

           A8: ( dom (i .--> B9)) = {i};

          set qc = (c9 +* (i .--> C9));

          ( dom qc) = I by A3, PZFMISC1: 1;

          then

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

          

           A9: ( dom (i .--> C9)) = {i};

          i in {i} by TARSKI:def 1;

          

          then

           A10: (qc . i) = ((i .--> C9) . i) by A9, FUNCT_4: 13

          .= C9 by FUNCOP_1: 72;

          

           A11: qc in M

          proof

            let j be object such that

             A12: j in I;

            now

              per cases ;

                case j = i;

                hence thesis by A7, A10;

              end;

                case j <> i;

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

                then (qc . j) = (c9 . j) by FUNCT_4: 11;

                hence thesis by A4, A12;

              end;

            end;

            hence thesis;

          end;

          set qb = (b9 +* (i .--> B9));

          ( dom qb) = I by A3, PZFMISC1: 1;

          then

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

          assume

           A13: not B9 c= C9;

          i in {i} by TARSKI:def 1;

          

          then

           A14: (qb . i) = ((i .--> B9) . i) by A8, FUNCT_4: 13

          .= B9 by FUNCOP_1: 72;

          qb in M

          proof

            let j be object such that

             A15: j in I;

            now

              per cases ;

                case j = i;

                hence thesis by A6, A14;

              end;

                case j <> i;

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

                then (qb . j) = (b9 . j) by FUNCT_4: 11;

                hence thesis by A5, A15;

              end;

            end;

            hence thesis;

          end;

          then qb c= qc or qc c= qb by A1, A11;

          hence thesis by A3, A13, A14, A10;

        end;

        then

        consider m9 be set such that

         A16: m9 in (M . i) & for D9 be set st D9 in (M . i) holds D9 c= m9 by A3, FINSET_1: 12;

        take m9;

        thus thesis by A16;

      end;

      consider m be ManySortedSet of I such that

       A17: for i be object st i in I holds Z[i, (m . i)] from PBOOLE:sch 3( A2);

      take m;

      thus m in M

      proof

        let i be object;

        assume i in I;

        then Z[i, (m . i)] by A17;

        hence thesis;

      end;

      thus for K be ManySortedSet of I st K in M holds K c= m

      proof

        let K be ManySortedSet of I such that

         A18: K in M;

        let i be object;

        assume

         A19: i in I;

        then

         A20: (K . i) in (M . i) by A18;

         Z[i, (m . i)] by A17, A19;

        hence thesis by A20;

      end;

    end;

    theorem :: MSSUBFAM:30

    Z is finite-yielding & Z c= ( rngs F) implies ex Y st Y c= ( doms F) & Y is finite-yielding & (F .:.: Y) = Z

    proof

      assume that

       A1: Z is finite-yielding and

       A2: Z c= ( rngs F);

      defpred P[ object, object] means ex A be set, f be Function st A = $2 & f = (F . $1) & A c= (( doms F) . $1) & A is finite & (f .: A) = (Z . $1);

      

       A3: for i be object st i in I holds ex j be object st P[i, j]

      proof

        let i be object;

        reconsider f = (F . i) as Function;

        assume

         A4: i in I;

        then ( rng f) = (( rngs F) . i) by Th13;

        then

         A5: (Z . i) c= ( rng f) by A2, A4;

        (Z . i) is finite by A1;

        then

        consider y be set such that

         A6: y c= ( dom f) & y is finite & (f .: y) = (Z . i) by A5, ORDERS_1: 85;

        take y, y, f;

        thus y = y;

        thus f = (F . i);

        thus thesis by A4, A6, Th14;

      end;

      consider Y be ManySortedSet of I such that

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

      take Y;

      thus Y c= ( doms F)

      proof

        let i be object;

        assume i in I;

        then P[i, (Y . i)] by A7;

        hence thesis;

      end;

      thus Y is finite-yielding

      proof

        let i be object;

        assume i in I;

        then P[i, (Y . i)] by A7;

        hence thesis;

      end;

      now

        let i be object;

        assume

         A8: i in I;

        then P[i, (Y . i)] by A7;

        hence ((F .:.: Y) . i) = (Z . i) by A8, PBOOLE:def 20;

      end;

      hence thesis;

    end;

    begin

    definition

      let I, M;

      mode MSSubsetFamily of M is ManySortedSubset of ( bool M);

    end

    registration

      let I, M;

      cluster non-empty for MSSubsetFamily of M;

      existence

      proof

        ( bool M) is ManySortedSubset of ( bool M) by PBOOLE:def 18;

        hence thesis;

      end;

    end

    definition

      let I, M;

      :: original: bool

      redefine

      func bool M -> MSSubsetFamily of M ;

      coherence by PBOOLE:def 18;

    end

    registration

      let I, M;

      cluster empty-yielding finite-yielding for MSSubsetFamily of M;

      existence

      proof

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

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

        hence thesis;

      end;

    end

    theorem :: MSSUBFAM:31

    ( EmptyMS I) is empty-yielding finite-yielding MSSubsetFamily of M by PBOOLE: 43, PBOOLE:def 18;

    registration

      let I;

      let M be finite-yielding ManySortedSet of I;

      cluster non-empty finite-yielding for MSSubsetFamily of M;

      existence

      proof

        ( bool M) is MSSubsetFamily of M;

        hence thesis;

      end;

    end

    reserve SF,SG,SH for MSSubsetFamily of M,

SFe for non-empty MSSubsetFamily of M,

V,W for ManySortedSubset of M;

    definition

      let I be non empty set, M be ManySortedSet of I, SF be MSSubsetFamily of M, i be Element of I;

      :: original: .

      redefine

      func SF . i -> Subset-Family of (M . i) ;

      coherence

      proof

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

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

        hence thesis by MBOOLEAN:def 1;

      end;

    end

    theorem :: MSSUBFAM:32

    

     Th32: i in I implies (SF . i) is Subset-Family of (M . i)

    proof

      assume

       A1: i in I;

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

      then (SF . i) c= (( bool M) . i) by A1;

      hence thesis by A1, MBOOLEAN:def 1;

    end;

    theorem :: MSSUBFAM:33

    

     Th33: A in SF implies A is ManySortedSubset of M

    proof

      

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

      assume A in SF;

      then A in ( bool M) by A1, PBOOLE: 9;

      then A c= M by MBOOLEAN: 18;

      hence thesis by PBOOLE:def 18;

    end;

    theorem :: MSSUBFAM:34

    

     Th34: (SF (\/) SG) is MSSubsetFamily of M

    proof

      SF c= ( bool M) & SG c= ( bool M) by PBOOLE:def 18;

      then (SF (\/) SG) c= ( bool M) by PBOOLE: 16;

      hence thesis by PBOOLE:def 18;

    end;

    theorem :: MSSUBFAM:35

    (SF (/\) SG) is MSSubsetFamily of M

    proof

      SF c= ( bool M) & SG c= ( bool M) by PBOOLE:def 18;

      then (SF (/\) SG) c= (( bool M) (/\) ( bool M)) by PBOOLE: 21;

      hence thesis by PBOOLE:def 18;

    end;

    theorem :: MSSUBFAM:36

    

     Th36: (SF (\) A) is MSSubsetFamily of M

    proof

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

      then

       A1: (SF (\) A) c= (( bool M) (\) A) by PBOOLE: 53;

      (( bool M) (\) A) c= ( bool M) by PBOOLE: 56;

      then (SF (\) A) c= ( bool M) by A1, PBOOLE: 13;

      hence thesis by PBOOLE:def 18;

    end;

    theorem :: MSSUBFAM:37

    (SF (\+\) SG) is MSSubsetFamily of M

    proof

      (SF (\) SG) is MSSubsetFamily of M & (SG (\) SF) is MSSubsetFamily of M by Th36;

      hence thesis by Th34;

    end;

    theorem :: MSSUBFAM:38

    

     Th38: A c= M implies {A} is MSSubsetFamily of M

    proof

      assume A c= M;

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

      then {A} c= ( bool M) by PZFMISC1: 33;

      hence thesis by PBOOLE:def 18;

    end;

    theorem :: MSSUBFAM:39

    

     Th39: A c= M & B c= M implies {A, B} is MSSubsetFamily of M

    proof

      assume A c= M & B c= M;

      then {A} is MSSubsetFamily of M & {B} is MSSubsetFamily of M by Th38;

      then ( {A} (\/) {B}) is MSSubsetFamily of M by Th34;

      hence thesis by PZFMISC1: 10;

    end;

    theorem :: MSSUBFAM:40

    

     Th40: ( union SF) c= M

    proof

      

       A1: for x be set holds for F be Subset-Family of x holds ( union F) is Subset of x;

      let i such that

       A2: i in I;

      (SF . i) is Subset-Family of (M . i) by A2, Th32;

      then ( union (SF . i)) is Subset of (M . i) by A1;

      then ( union (SF . i)) c= (M . i);

      hence thesis by A2, MBOOLEAN:def 2;

    end;

    begin

    definition

      let I, M, SF;

      :: MSSUBFAM:def1

      func meet SF -> ManySortedSet of I means

      : Def1: for i be object st i in I holds ex Q be Subset-Family of (M . i) st Q = (SF . i) & (it . i) = ( Intersect Q);

      existence

      proof

        defpred Z[ object, object] means ex Q be Subset-Family of (M . $1) st Q = (SF . $1) & $2 = ( Intersect Q);

        

         A1: for i be object st i in I holds ex j be object st Z[i, j]

        proof

          let i be object;

          assume

           A2: i in I;

          then

          reconsider Q = (SF . i) as Subset-Family of (M . i) by Th32;

          reconsider a = (I --> ( Intersect Q)) as ManySortedSet of I;

          take (a . i);

          take Q;

          thus thesis by A2, FUNCOP_1: 7;

        end;

        ex X be ManySortedSet of I st for i be object st i in I holds Z[i, (X . i)] from PBOOLE:sch 3( A1);

        hence thesis;

      end;

      uniqueness

      proof

        let X1,X2 be ManySortedSet of I such that

         A3: (for i be object st i in I holds ex Q1 be Subset-Family of (M . i) st Q1 = (SF . i) & (X1 . i) = ( Intersect Q1)) & for i be object st i in I holds ex Q2 be Subset-Family of (M . i) st Q2 = (SF . i) & (X2 . i) = ( Intersect Q2);

        now

          let i be object;

          assume i in I;

          then (ex Q1 be Subset-Family of (M . i) st Q1 = (SF . i) & (X1 . i) = ( Intersect Q1)) & ex Q2 be Subset-Family of (M . i) st Q2 = (SF . i) & (X2 . i) = ( Intersect Q2) by A3;

          hence (X1 . i) = (X2 . i);

        end;

        hence X1 = X2;

      end;

    end

    definition

      let I, M, SF;

      :: original: meet

      redefine

      func meet SF -> ManySortedSubset of M ;

      coherence

      proof

        let i be object;

        assume i in I;

        then ex Q be Subset-Family of (M . i) st Q = (SF . i) & (( meet SF) . i) = ( Intersect Q) by Def1;

        hence thesis;

      end;

    end

    theorem :: MSSUBFAM:41

    

     Th41: SF = ( EmptyMS I) implies ( meet SF) = M

    proof

      assume

       A1: SF = ( EmptyMS I);

      now

        let i be object;

        assume i in I;

        then

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

         A2: Q = (SF . i) and

         A3: (( meet SF) . i) = ( Intersect Q) by Def1;

        Q = {} by A1, A2;

        hence (( meet SF) . i) = (M . i) by A3, SETFAM_1:def 9;

      end;

      hence thesis;

    end;

    theorem :: MSSUBFAM:42

    ( meet SFe) c= ( union SFe)

    proof

      let i be object;

      assume

       A1: i in I;

      then

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

       A2: Q = (SFe . i) and

       A3: (( meet SFe) . i) = ( Intersect Q) by Def1;

      ( meet Q) c= ( union Q) & ( Intersect Q) = ( meet Q) by A1, A2, SETFAM_1: 2, SETFAM_1:def 9;

      hence thesis by A1, A2, A3, MBOOLEAN:def 2;

    end;

    theorem :: MSSUBFAM:43

    A in SF implies ( meet SF) c= A

    proof

      assume

       A1: A in SF;

      let i be object;

      assume

       A2: i in I;

      then

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

       A3: Q = (SF . i) and

       A4: (( meet SF) . i) = ( Intersect Q) by Def1;

      

       A5: (A . i) in (SF . i) by A1, A2;

      then ( Intersect Q) = ( meet Q) by A3, SETFAM_1:def 9;

      hence thesis by A3, A4, A5, SETFAM_1: 3;

    end;

    theorem :: MSSUBFAM:44

    ( EmptyMS I) in SF implies ( meet SF) = ( EmptyMS I)

    proof

      assume

       A1: ( EmptyMS I) in SF;

      now

        let i be object;

        assume

         A2: i in I;

        then

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

         A3: Q = (SF . i) and

         A4: (( meet SF) . i) = ( Intersect Q) by Def1;

        (( EmptyMS I) . i) in Q by A1, A2, A3;

        then

         A5: {} in Q;

        (( EmptyMS I) . i) in (SF . i) by A1, A2;

        then ( Intersect Q) = ( meet Q) by A3, SETFAM_1:def 9;

        then ( Intersect Q) = {} by A5, SETFAM_1: 4;

        hence (( meet SF) . i) = (( EmptyMS I) . i) by A4;

      end;

      hence thesis;

    end;

    theorem :: MSSUBFAM:45

    for Z,M be ManySortedSet of I holds for SF be non-empty MSSubsetFamily 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,M be ManySortedSet of I, SF be non-empty MSSubsetFamily of M such that

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

      let i be object;

      consider T be ManySortedSet of I such that

       A2: T in SF by PBOOLE: 134;

      assume

       A3: i in I;

      then

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

       A4: Q = (SF . i) and

       A5: (( meet SF) . i) = ( Intersect Q) by Def1;

      

       A6: for Z9 be set st Z9 in Q holds (Z . i) c= Z9

      proof

        let Z9 be set such that

         A7: Z9 in Q;

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

        then

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

        

         A8: ( dom (i .--> Z9)) = {i};

        i in {i} by TARSKI:def 1;

        

        then

         A9: (K . i) = ((i .--> Z9) . i) by A8, FUNCT_4: 13

        .= Z9 by FUNCOP_1: 72;

        K in SF

        proof

          let q be object such that

           A10: q in I;

          per cases ;

            suppose q = i;

            hence thesis by A4, A7, A9;

          end;

            suppose q <> i;

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

            then (K . q) = (T . q) by FUNCT_4: 11;

            hence thesis by A2, A10;

          end;

        end;

        then Z c= K by A1;

        hence thesis by A3, A9;

      end;

      ( Intersect Q) = ( meet Q) by A3, A4, SETFAM_1:def 9;

      hence thesis by A3, A4, A5, A6, SETFAM_1: 5;

    end;

    theorem :: MSSUBFAM:46

    SF c= SG implies ( meet SG) c= ( meet SF)

    proof

      assume

       A1: SF c= SG;

      let i be object;

      assume

       A2: i in I;

      then

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

       A3: Qf = (SF . i) and

       A4: (( meet SF) . i) = ( Intersect Qf) by Def1;

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

       A5: Qg = (SG . i) and

       A6: (( meet SG) . i) = ( Intersect Qg) by A2, Def1;

      Qf c= Qg by A1, A2, A3, A5;

      hence thesis by A4, A6, SETFAM_1: 44;

    end;

    theorem :: MSSUBFAM:47

    A in SF & A c= B implies ( meet SF) c= B

    proof

      assume that

       A1: A in SF and

       A2: A c= B;

      let i be object;

      assume

       A3: i in I;

      then

       A4: (A . i) c= (B . i) by A2;

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

       A5: Q = (SF . i) and

       A6: (( meet SF) . i) = ( Intersect Q) by A3, Def1;

      

       A7: (A . i) in (SF . i) by A1, A3;

      then ( Intersect Q) = ( meet Q) by A5, SETFAM_1:def 9;

      hence thesis by A5, A6, A7, A4, SETFAM_1: 7;

    end;

    theorem :: MSSUBFAM:48

    A in SF & (A (/\) B) = ( EmptyMS I) implies (( meet SF) (/\) B) = ( EmptyMS I)

    proof

      assume that

       A1: A in SF and

       A2: (A (/\) B) = ( EmptyMS I);

      now

        let i be object;

        assume

         A3: i in I;

        then

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

         A4: Q = (SF . i) and

         A5: (( meet SF) . i) = ( Intersect Q) by Def1;

        

         A6: (A . i) in (SF . i) by A1, A3;

        ((A . i) /\ (B . i)) = (( EmptyMS I) . i) by A2, A3, PBOOLE:def 5;

        then ((A . i) /\ (B . i)) = {} ;

        then (A . i) misses (B . i);

        then ( meet Q) misses (B . i) by A4, A6, SETFAM_1: 8;

        then (( meet Q) /\ (B . i)) = {} ;

        then

         A7: (( meet Q) /\ (B . i)) = (( EmptyMS I) . i);

        ( Intersect Q) = ( meet Q) by A4, A6, SETFAM_1:def 9;

        hence ((( meet SF) (/\) B) . i) = (( EmptyMS I) . i) by A3, A5, A7, PBOOLE:def 5;

      end;

      hence thesis;

    end;

    theorem :: MSSUBFAM:49

    SH = (SF (\/) SG) implies ( meet SH) = (( meet SF) (/\) ( meet SG))

    proof

      assume

       A1: SH = (SF (\/) SG);

      now

        let i be object;

        assume

         A2: i in I;

        then

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

         A3: Qf = (SF . i) and

         A4: (( meet SF) . i) = ( Intersect Qf) by Def1;

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

         A5: Qh = (SH . i) and

         A6: (( meet SH) . i) = ( Intersect Qh) by A2, Def1;

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

         A7: Qg = (SG . i) and

         A8: (( meet SG) . i) = ( Intersect Qg) by A2, Def1;

        

         A9: Qh = (Qf \/ Qg) by A1, A2, A3, A7, A5, PBOOLE:def 4;

        now

          per cases ;

            case

             A10: Qf <> {} & Qg <> {} ;

            

            hence (( meet SH) . i) = ( meet Qh) by A6, A9, SETFAM_1:def 9

            .= (( meet Qf) /\ ( meet Qg)) by A9, A10, SETFAM_1: 9

            .= ((( meet SF) . i) /\ ( meet Qg)) by A4, A10, SETFAM_1:def 9

            .= ((( meet SF) . i) /\ (( meet SG) . i)) by A8, A10, SETFAM_1:def 9

            .= ((( meet SF) (/\) ( meet SG)) . i) by A2, PBOOLE:def 5;

          end;

            case

             A11: Qf <> {} & Qg = {} ;

            

            hence (( meet SH) . i) = ((( meet SF) . i) /\ (M . i)) by A4, A6, A9, XBOOLE_1: 28

            .= ((( meet SF) . i) /\ (( meet SG) . i)) by A8, A11, SETFAM_1:def 9

            .= ((( meet SF) (/\) ( meet SG)) . i) by A2, PBOOLE:def 5;

          end;

            case

             A12: Qf = {} & Qg <> {} ;

            

            hence (( meet SH) . i) = ((M . i) /\ (( meet SG) . i)) by A8, A6, A9, XBOOLE_1: 28

            .= ((( meet SF) . i) /\ (( meet SG) . i)) by A4, A12, SETFAM_1:def 9

            .= ((( meet SF) (/\) ( meet SG)) . i) by A2, PBOOLE:def 5;

          end;

            case Qf = {} & Qg = {} ;

            

            hence (( meet SH) . i) = (( Intersect Qf) /\ ( Intersect Qg)) by A6, A9

            .= ((( meet SF) (/\) ( meet SG)) . i) by A2, A4, A8, PBOOLE:def 5;

          end;

        end;

        hence (( meet SH) . i) = ((( meet SF) (/\) ( meet SG)) . i);

      end;

      hence thesis;

    end;

    theorem :: MSSUBFAM:50

    SF = {V} implies ( meet SF) = V

    proof

      assume

       A1: SF = {V};

      now

        let i be object;

        assume

         A2: i in I;

        then

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

         A3: Q = (SF . i) and

         A4: (( meet SF) . i) = ( Intersect Q) by Def1;

        

        thus (( meet SF) . i) = ( meet Q) by A1, A2, A3, A4, SETFAM_1:def 9

        .= ( meet {(V . i)}) by A1, A2, A3, PZFMISC1:def 1

        .= (V . i) by SETFAM_1: 10;

      end;

      hence thesis;

    end;

    theorem :: MSSUBFAM:51

    

     Th51: SF = {V, W} implies ( meet SF) = (V (/\) W)

    proof

      assume

       A1: SF = {V, W};

      now

        let i be object;

        assume

         A2: i in I;

        then ex Q be Subset-Family of (M . i) st Q = (SF . i) & (( meet SF) . i) = ( Intersect Q) by Def1;

        

        hence (( meet SF) . i) = ( meet ( {V, W} . i)) by A1, A2, SETFAM_1:def 9

        .= ( meet {(V . i), (W . i)}) by A2, PZFMISC1:def 2

        .= ((V . i) /\ (W . i)) by SETFAM_1: 11

        .= ((V (/\) W) . i) by A2, PBOOLE:def 5;

      end;

      hence thesis;

    end;

    theorem :: MSSUBFAM:52

    A in ( meet SF) implies for B st B in SF holds A in B

    proof

      assume

       A1: A in ( meet SF);

      let B such that

       A2: B in SF;

      let i be object;

      assume

       A3: i in I;

      then

       A4: (A . i) in (( meet SF) . i) by A1;

      

       A5: (B . i) in (SF . i) by A2, A3;

      ex Q be Subset-Family of (M . i) st Q = (SF . i) & (( meet SF) . i) = ( Intersect Q) by A3, Def1;

      hence thesis by A4, A5, SETFAM_1: 43;

    end;

    theorem :: MSSUBFAM:53

    for A,M be ManySortedSet of I holds for SF be non-empty MSSubsetFamily of M st (A in M & for B be ManySortedSet of I st B in SF holds A in B) holds A in ( meet SF)

    proof

      let A,M be ManySortedSet of I, SF be non-empty MSSubsetFamily of M;

      assume that

       A1: A in M and

       A2: for B be ManySortedSet of I st B in SF holds A in B;

      let i be object;

      consider T be ManySortedSet of I such that

       A3: T in SF by PBOOLE: 134;

      assume

       A4: i in I;

      then

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

       A5: Q = (SF . i) and

       A6: (( meet SF) . i) = ( Intersect Q) by Def1;

      

       A7: for B9 be set st B9 in Q holds (A . i) in B9

      proof

        let B9 be set such that

         A8: B9 in Q;

        ( dom (T +* (i .--> B9))) = I by A4, PZFMISC1: 1;

        then

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

        

         A9: ( dom (i .--> B9)) = {i};

        i in {i} by TARSKI:def 1;

        

        then

         A10: (K . i) = ((i .--> B9) . i) by A9, FUNCT_4: 13

        .= B9 by FUNCOP_1: 72;

        K in SF

        proof

          let q be object such that

           A11: q in I;

          per cases ;

            suppose q = i;

            hence thesis by A5, A8, A10;

          end;

            suppose q <> i;

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

            then (K . q) = (T . q) by FUNCT_4: 11;

            hence thesis by A3, A11;

          end;

        end;

        then A in K by A2;

        hence thesis by A4, A10;

      end;

      (A . i) in (M . i) by A1, A4;

      hence thesis by A6, A7, SETFAM_1: 43;

    end;

    definition

      let I, M;

      let IT be MSSubsetFamily of M;

      :: MSSUBFAM:def2

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

      :: MSSUBFAM:def3

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

      :: MSSUBFAM:def4

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

      :: MSSUBFAM:def5

      attr IT is absolutely-multiplicative means for F be MSSubsetFamily of M st F c= IT holds ( meet F) in IT;

      :: MSSUBFAM:def6

      attr IT is properly-upper-bound means M in IT;

      :: MSSUBFAM:def7

      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

      proof

        let A, B;

        assume A in ( bool M) & B in ( bool M);

        then A c= M & B c= M by MBOOLEAN: 1;

        then (A (\/) B) c= M by PBOOLE: 16;

        hence (A (\/) B) in ( bool M) by MBOOLEAN: 1;

      end;

      thus ( bool M) is absolutely-additive by Th40, MBOOLEAN: 18;

      thus ( bool M) is multiplicative

      proof

        let A, B;

        assume that

         A1: A in ( bool M) and B in ( bool M);

        A c= M by A1, MBOOLEAN: 1;

        then (A (/\) B) c= M by MBOOLEAN: 14;

        hence thesis by MBOOLEAN: 1;

      end;

      thus ( bool M) is absolutely-multiplicative by PBOOLE:def 18, MBOOLEAN: 18;

      M in ( bool M) by MBOOLEAN: 18;

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

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

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

      hence ( bool M) is properly-lower-bound;

    end;

    registration

      let I, M;

      cluster non-empty additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound for MSSubsetFamily 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 MSSubsetFamily of M ;

      coherence by Lm1;

    end

    registration

      let I, M;

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

      coherence

      proof

        let SF be MSSubsetFamily of M such that

         A1: SF is absolutely-additive;

        let A, B;

        assume that

         A2: A in SF and

         A3: B in SF;

         {A} c= SF & {B} c= SF by A2, A3, PZFMISC1: 33;

        then ( {A} (\/) {B}) c= SF by PBOOLE: 16;

        then

         A4: {A, B} c= SF by PZFMISC1: 10;

        B is ManySortedSubset of M by A3, Th33;

        then

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

        A is ManySortedSubset of M by A2, Th33;

        then A c= M by PBOOLE:def 18;

        then {A, B} is MSSubsetFamily of M by A5, Th39;

        then ( union {A, B}) in SF by A1, A4;

        hence thesis by PZFMISC1: 32;

      end;

    end

    registration

      let I, M;

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

      coherence

      proof

        let SF be MSSubsetFamily of M such that

         A1: SF is absolutely-multiplicative;

        let A, B;

        assume that

         A2: A in SF and

         A3: B in SF;

        

         A4: B is ManySortedSubset of M by A3, Th33;

        then

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

        

         A6: A is ManySortedSubset of M by A2, Th33;

        then A c= M by PBOOLE:def 18;

        then

        reconsider ab = {A, B} as MSSubsetFamily of M by A5, Th39;

         {A} c= SF & {B} c= SF by A2, A3, PZFMISC1: 33;

        then ( {A} (\/) {B}) c= SF by PBOOLE: 16;

        then {A, B} c= SF by PZFMISC1: 10;

        then ( meet ab) in SF by A1;

        hence thesis by A6, A4, Th51;

      end;

    end

    registration

      let I, M;

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

      coherence

      proof

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

        then

        reconsider a = ( EmptyMS I) as MSSubsetFamily of M by PBOOLE:def 18;

        let SF be MSSubsetFamily of M such that

         A1: SF is absolutely-multiplicative;

        ( meet a) = M & ( EmptyMS I) c= SF by Th41, PBOOLE: 43;

        hence M in SF by A1;

      end;

    end

    registration

      let I, M;

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

      coherence

      proof

        let SF be MSSubsetFamily of M;

        assume SF is properly-upper-bound;

        then

         A1: M in SF;

        let i be object;

        assume i in I;

        hence thesis by A1;

      end;

    end

    registration

      let I, M;

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

      coherence

      proof

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

        then

        reconsider a = ( EmptyMS I) as MSSubsetFamily of M by PBOOLE:def 18;

        let SF be MSSubsetFamily of M such that

         A1: SF is absolutely-additive;

        ( union a) = ( EmptyMS I) & ( EmptyMS I) c= SF by PBOOLE: 43;

        hence ( EmptyMS I) in SF by A1;

      end;

    end

    registration

      let I, M;

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

      coherence

      proof

        let SF be MSSubsetFamily of M;

        assume SF is properly-lower-bound;

        then

         A1: ( EmptyMS I) in SF;

        let i be object;

        assume i in I;

        hence thesis by A1;

      end;

    end