:: Certain Facts about Families of Subsets of Many Sorted Sets
::  by Artur Korni{\l}owicz
::
:: Received October 27, 1995
:: Copyright (c) 1995-2019 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies PBOOLE, FUNCT_6, RELAT_1, PARTFUN1, FUNCT_1, SETFAM_1, SUBSET_1,
      FINSET_1, XBOOLE_0, TARSKI, MEMBER_1, PZFMISC1, ZFMISC_1, FUNCT_4,
      FUNCOP_1, FUNCT_2, ORDINAL1, MSSUBFAM, SETLIM_2;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, RELAT_1, FUNCT_1,
      ORDINAL1, PARTFUN1, FUNCT_2, FUNCOP_1, FINSET_1, FUNCT_4, FUNCT_6,
      PBOOLE, MBOOLEAN, PZFMISC1;
 constructors SETFAM_1, FUNCT_4, FUNCT_6, MBOOLEAN, PZFMISC1, PARTFUN1,
      RELSET_1, ORDINAL1, PBOOLE, FINSET_1;
 registrations XBOOLE_0, FUNCT_1, FUNCOP_1, FINSET_1, PBOOLE, PRE_CIRC,
      MBOOLEAN, PZFMISC1, FUNCT_2, PARTFUN1, CARD_1, RELSET_1, RELAT_1;
 requirements SUBSET, BOOLE;
 definitions XBOOLE_0, PBOOLE, FINSET_1, ORDINAL1;
 equalities PBOOLE, FUNCOP_1;
 expansions XBOOLE_0, PBOOLE;
 theorems FUNCOP_1, FINSET_1, ORDERS_1, FRAENKEL, FUNCT_2, FUNCT_4, FUNCT_6,
      MBOOLEAN, PBOOLE, PZFMISC1, SETFAM_1, TARSKI, RELSET_1, XBOOLE_0,
      XBOOLE_1, RELAT_1, PARTFUN1;
 schemes FUNCT_2, PBOOLE;

begin :: Preliminaries

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 for I-defined Function;
  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 for I-defined Function;
  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
  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() for x be object st x in A().i
   ex y be object st y in B().i & P[y,x,i]
proof
  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
      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 :: SETFAM_1:3
  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 :: SETFAM_1:4
  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 :: SETFAM_1:5
  {} 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 :: SETFAM_1:6
  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 :: SETFAM_1:6
  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 :: SETFAM_1:8
  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 :: SETFAM_1:9
  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 :: SETFAM_1:10
  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 :: SETFAM_1:11
  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 :: SETFAM_1:12
  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
  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
  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 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 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
  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
  for A be non-empty ManySortedSet of I 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
  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 :: Finite Many Sorted Sets

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 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 :: FINSET_1:22
  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 :: FINSET_1:23
  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 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
  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
  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 :: FINSET_1:26
  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 :: FINSET_1:27
  (A c= rngs F & for i be set 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 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 :: CQC_THE1:13
  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 being object st i in I 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 being 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 being object st i in I holds Q[i,A.i] from PBOOLE:sch 3(A3);
  defpred P[object,object] means
  ex D being 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 being object st i in I 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 being 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 :: CQC_THE1:14
  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 being set st D = $2 & D is finite & D c= Y.$1 & X.$1 c= [:D,Z.$1:];
A3: for i being object st i in I 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 being 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
  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 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 being set st D = $2 &
   $2 in M.$1 & for D9 be set st D9 in M.$1 holds D c= D9;
A2: for i being object st i in I 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 being 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 :: FIN_TOPO:3
  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 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 being set st X = $2 &
   $2 in M.$1 & for D9 be set st D9 in M.$1 holds D9 c= X;
A2: for i being object st i in I 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 being 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 :: COMPTS_1:1
  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 being 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 being object st i in I 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 being 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 :: A Family of Subsets of Many Sorted Sets

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;
  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
  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;
  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 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 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 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
  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 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
  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 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 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 Th40:
  union SF c= M
proof
A1: for x being set
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 :: Intersection of a Family of Many Sorted Sets

definition
  let I, M, SF;

  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 being object st i in I 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 being object st i in I
     ex Q1 be Subset-Family of M.i st Q1 = SF.i & X1.i = Intersect Q1)
 & for i being object st i in I 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;
  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 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 :: SETFAM_1:3
  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,def 9;
  hence thesis by A1,A2,A3,MBOOLEAN:def 2;
end;

theorem :: SETFAM_1:4
  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 :: SETFAM_1:5
  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 :: SETFAM_1:6
  for Z, M be ManySortedSet of I 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 :: SETFAM_1:7 :: SETFAM_1:59
  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 :: SETFAM_1:8
  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 :: SETFAM_1:9
  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 :: SETFAM_1:10
  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 :: SETFAM_1:11
  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 Th51: :: SETFAM_1:12
  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
  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
  for A, M be ManySortedSet of I 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;
  attr IT is additive means
  for A, B st A in IT & B in IT holds A (\/) B in IT;
  attr IT is absolutely-additive means

  for F be MSSubsetFamily of M st F c= IT holds union F in IT;
  attr IT is multiplicative means
  for A, B st A in IT & B in IT holds A (/\) B in IT;
  attr IT is absolutely-multiplicative means

  for F be MSSubsetFamily of M st F c= IT holds meet F in IT;
  attr IT is properly-upper-bound means

  M in IT;
  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;
  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;