The Mizar article:

A Theory of Partitions. Part I

by
Shunichi Kobayashi, and
Kui Jia

Received October 5, 1998

Copyright (c) 1998 Association of Mizar Users

MML identifier: PARTIT1
[ MML identifier index ]


environ

 vocabulary EQREL_1, BOOLE, SETFAM_1, TARSKI, CANTOR_1, FUNCT_1, RELAT_1,
      T_1TOPSP, SUBSET_1, FINSEQ_1, ARYTM_1, LATTICES, PUA2MSS1, PARTIT1;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, XCMPLX_0, XREAL_0, NAT_1,
      RELAT_1, FUNCT_1, FUNCT_2, SETFAM_1, PUA2MSS1, FINSEQ_1, FINSEQ_4,
      EQREL_1, CANTOR_1, T_1TOPSP;
 constructors NAT_1, FINSEQ_4, PUA2MSS1, CANTOR_1, T_1TOPSP, XREAL_0, MEMBERED;
 clusters SUBSET_1, RELSET_1, ARYTM_3, SETFAM_1, MEMBERED, EQREL_1, PARTFUN1;
 requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
 definitions TARSKI, RELAT_1;
 theorems TARSKI, FUNCT_1, SETFAM_1, EQREL_1, AXIOMS, LATTICE4, ZFMISC_1,
      PUA2MSS1, RELAT_1, MSUALG_5, NAT_1, FINSEQ_1, FINSEQ_2, CQC_THE1,
      CANTOR_1, FUNCT_2, T_1TOPSP, SUBSET_1, RELSET_1, XBOOLE_0, XBOOLE_1,
      XCMPLX_1;
 schemes EQREL_1, NAT_1, ZFREFLE1, COMPLSP1, XBOOLE_0;

begin

::Chap. 1  Preliminaries

reserve Y,Z for non empty set;
reserve PA,PB for a_partition of Y;
reserve A,B for Subset of Y;
reserve i,j,k for Nat;
reserve x,y,z,x1,x2,y1,z0,X,V,a,b,d,t,SFX,SFY for set;

theorem Th1:X in PA & V in PA & X c= V implies X=V
proof
  assume A1: X in PA & V in PA & X c= V;
  then A2: X=V or X misses V by EQREL_1:def 6;
  consider x being Element of X;
    X<>{} by A1,EQREL_1:def 6;
  then x in X;
  hence X=V by A1,A2,XBOOLE_0:3;
end;

definition let SFX,SFY;
 redefine pred SFX is_finer_than SFY;
 synonym SFX '<' SFY;
 synonym SFY '>' SFX;
end;

canceled;

theorem Th3:
   union (SFX \ {{}}) = union SFX
proof
  A1: union (SFX \ {{}}) c= (union SFX)
  proof
    let y be set;
    assume y in union (SFX \ {{}});
    then consider z being set such that A2: y in z & z in (SFX \{{}
}) by TARSKI:def 4;
      z in SFX & not z in {{}} by A2,XBOOLE_0:def 4;
    hence y in union SFX by A2,TARSKI:def 4;
  end;
    union SFX c= union (SFX \ {{}})
  proof
    let y be set;
    assume y in union SFX;
    then consider X being set such that A3: y in X & X in SFX by TARSKI:def 4;
      not X in {{}} by A3,TARSKI:def 1;
    then X in SFX \ {{}} by A3,XBOOLE_0:def 4;
    hence thesis by A3,TARSKI:def 4;
  end;
  hence thesis by A1,XBOOLE_0:def 10;
end;

theorem Th4: for PA,PB being a_partition of Y st
  PA '>' PB & PB '>' PA holds PB c= PA
proof let PA,PB be a_partition of Y;
  assume A1: PA '>' PB & PB '>' PA;
  let x be set;assume A2:x in PB;
  then consider V such that A3: V in PA & x c= V by A1,SETFAM_1:def 2;
  consider W being set such that A4: W in PB & V c= W
                         by A1,A3,SETFAM_1:def 2;
    x c= W by A3,A4,XBOOLE_1:1;
  then x=W by A2,A4,Th1;
  hence x in PA by A3,A4,XBOOLE_0:def 10;
end;

theorem Th5: for PA,PB being a_partition of Y st
  PA '>' PB & PB '>' PA holds PA = PB
proof let PA,PB be a_partition of Y;
  assume A1: PA '>' PB & PB '>' PA;
  then A2:PB c= PA by Th4;
    PA c= PB by A1,Th4;
  hence PA = PB by A2,XBOOLE_0:def 10;
end;

canceled;

theorem Th7: for PA,PB being a_partition of Y st
  PA '>' PB holds PA is_coarser_than PB
proof
  let PA,PB be a_partition of Y;
  assume A1:PA '>' PB;
    for x being set st x in PA ex y being set st y in PB & y c= x
  proof
    let x be set;
    assume A2:x in PA;
    then A3:x<>{} by EQREL_1:def 6;
    consider u being Element of x;
    A4:u in x by A3;
      union PB = Y by EQREL_1:def 6;
    then consider y being set such that A5: u in y & y in PB by A2,A4,TARSKI:
def 4;
    consider z being set such that A6:z in PA & y c= z by A1,A5,SETFAM_1:def 2;
      x=z or x misses z by A2,A6,EQREL_1:def 6;
    hence ex y1 being set st y1 in PB & y1 c= x by A3,A5,A6,XBOOLE_0:3;
  end;
  hence PA is_coarser_than PB by SETFAM_1:def 3;
end;

definition let Y;let PA be a_partition of Y,b be set;
 pred b is_a_dependent_set_of PA means
 :Def1: ex B being set st B c= PA & B<>{} & b = union B;
end;

definition let Y;let PA,PB be a_partition of Y,b be set;
  pred b is_min_depend PA,PB means
  :Def2: b is_a_dependent_set_of PA &
   b is_a_dependent_set_of PB &
  for d being set st d c= b
    & d is_a_dependent_set_of PA &
      d is_a_dependent_set_of PB holds d=b;
end;

theorem Th8: for PA,PB being a_partition of Y
   st PA '>' PB holds for b being set st b in PA holds
      b is_a_dependent_set_of PB
proof
  let PA,PB be a_partition of Y;
  assume A1:PA '>' PB;
  A2:union PB = Y & for A st A in PB holds A<>{} &
    for B st B in PB holds A = B or A misses B by EQREL_1:def 6;
A3: PA is_coarser_than PB by A1,Th7;
    for b being set st b in PA holds b is_a_dependent_set_of PB
  proof
    let b be set;
    assume A4:b in PA;
    set B0={x8 where x8 is Element of bool Y: x8 in PB & x8 c= b};
    consider xb be set such that A5:xb in PB & xb c= b by A3,A4,SETFAM_1:def 3;
A6: xb in B0 by A5;
      z in B0 implies z in PB
    proof
      assume z in B0;
      then ex x8 being Element of bool Y st x8=z & x8 in PB & x8 c= b;
      hence thesis;
    end;
    then A7:B0 c= PB by TARSKI:def 3;
      z in b implies z in union B0
    proof
      assume A8:z in b;
      then consider x1 such that A9:z in x1 & x1 in PB by A2,A4,TARSKI:def 4;
      consider y1 such that A10:y1 in PA & x1 c= y1 by A1,A9,SETFAM_1:def 2;
         b = y1 or b misses y1 by A4,A10,EQREL_1:def 6;
      then x1 in B0 & z in x1 by A8,A9,A10,XBOOLE_0:3;
      hence z in union B0 by TARSKI:def 4;
    end;
    then A11:b c= union B0 by TARSKI:def 3;
      z in union B0 implies z in b
    proof
      assume z in union B0;
      then consider y such that A12:z in y & y in B0 by TARSKI:def 4;
        ex x8 being Element of bool Y st x8=y & (x8 in PB & x8 c= b) by A12;
      hence z in b by A12;
    end;
    then union B0 c= b by TARSKI:def 3;
    then b = union B0 by A11,XBOOLE_0:def 10;
    hence thesis by A6,A7,Def1;
  end;
  hence thesis;
end;

theorem Th9:
for PA being a_partition of Y holds
    Y is_a_dependent_set_of PA
proof
  let PA be a_partition of Y;
    {Y} c= bool Y by ZFMISC_1:80;
  then A1:{Y} is Subset-Family of Y by SETFAM_1:def 7;
  A2:union {Y} = Y by ZFMISC_1:31;
    for A st A in {Y} holds A<>{} &
  for B st B in {Y} holds A = B or A misses B
  proof
    let A;
    assume A3: A in {Y};
    then A4:A=Y by TARSKI:def 1;
    thus A<>{} by A3,TARSKI:def 1;
    let B;
    assume B in {Y};
    hence thesis by A4,TARSKI:def 1;
  end;
  then A5:{Y} is a_partition of Y by A1,A2,EQREL_1:def 6;
  A6:{Y} '>' PA
  proof
      for a being set st a in PA
            ex b being set st b in {Y} & a c= b
    proof
      let a be set;
      assume A7: a in PA;
      then A8: a c= Y & a<>{} by EQREL_1:def 6;
      consider x being Element of a;
        x in Y by A8,TARSKI:def 3;
      then consider b being set such that
      A9: x in b & b in {Y} by A2,TARSKI:def 4;
        b = Y by A9,TARSKI:def 1;
      hence thesis by A7,A9;
    end;
    hence thesis by SETFAM_1:def 2;
  end;
       Y in {Y} by TARSKI:def 1;
  hence Y is_a_dependent_set_of PA by A5,A6,Th8;
end;

theorem Th10:
for F being Subset-Family of Y st (Intersect(F)<>{} &
   for X st X in F holds X is_a_dependent_set_of PA)
    holds (Intersect(F) is_a_dependent_set_of PA)
proof
 let F be Subset-Family of Y;
 per cases;
 suppose F={};
  then Intersect(F)=Y by CANTOR_1:def 3;
  hence thesis by Th9;
 suppose A1:F<>{};
   then reconsider F' = F as non empty Subset-Family of Y;
  assume A2:Intersect(F)<>{} &
             for X st X in F holds X is_a_dependent_set_of PA;
  defpred P[set,set] means $2 c= PA & $2<>{} & $1=union $2;
  A3:for X st X in F holds ex B being set st P[X,B]
  proof
    let X;
    assume X in F;
    then X is_a_dependent_set_of PA by A2;
    hence ex B being set st B c= PA & B<>{} & X=union B by Def1;
  end;
  consider f being Function such that
    A4:dom f = F & for X st X in F holds P[X,f.X] from NonUniqFuncEx(A3);
    rng f c= bool bool Y
  proof
    let y be set;
    assume y in rng f;
    then consider x being set such that
      A5:x in dom f & y = f.x by FUNCT_1:def 5;
      f.x c= PA by A4,A5;
    then y c= bool Y by A5,XBOOLE_1:1;
    hence thesis;
  end;
  then reconsider f as Function of F', bool bool Y
    by A4,FUNCT_2:def 1,RELSET_1:11;
  defpred P[set] means $1 in F;
  deffunc S(Element of F') = f.$1;
  reconsider T={S(X) where X is Element of F':P[X]}
    as Subset of bool bool Y from SubsetFD;
  reconsider T as Subset-Family of bool Y by SETFAM_1:def 7;
  take B=Intersect(T);
  thus B c= PA
  proof
    let x;
    assume A6:x in B;
    consider X being set such that
      A7:X in F by A1,XBOOLE_0:def 1;
      f.X in T by A7;
    then A8:x in f.X by A6,CANTOR_1:10;
      f.X c= PA by A4,A7;
    hence x in PA by A8;
  end;
  thus B<>{}
  proof
    consider X being set such that
      A9:X in F by A1,XBOOLE_0:def 1;
A10: f.X in T by A9;
    consider A being set such that
      A11:A in Intersect(F) by A2,XBOOLE_0:def 1;
    reconsider A as Element of Y by A11;
    set AA = EqClass(A,PA);
A12: A in meet F by A1,A11,CANTOR_1:def 3;
      for X st X in T holds AA in X
    proof
      let X;
      assume X in T;
      then consider z being Element of F' such that
        A13:X=f.z & z in F;
      A14:f.z c= PA by A4;
      A15:z = union (f.z) by A4;
        A in z by A12,SETFAM_1:def 1;
      then ex A0 being set st A in A0 & A0 in f.z by A15,TARSKI:def 4;
      hence AA in X by A13,A14,T_1TOPSP:def 1;
    end;
    then EqClass(A,PA) in meet T by A10,SETFAM_1:def 1;
    hence thesis by A10,CANTOR_1:def 3;
  end;
  thus Intersect(F) = union B
  proof
    A16:Intersect(F) c= union B
    proof
      let x be set;
      assume A17:x in Intersect(F);
then A18:  x in meet F by A1,CANTOR_1:def 3;
      reconsider x as Element of Y by A17;
      reconsider PA as a_partition of Y;
      set A = EqClass(x,PA);
      consider X being set such that
        A19:X in F by A1,XBOOLE_0:def 1;
A20:  f.X in T by A19;
A21:   x in A by T_1TOPSP:def 1;
        for X st X in T holds A in X
      proof
        let X;
        assume X in T;
        then consider z being Element of F' such that
          A22:X=f.z & z in F;
        A23:f.z c= PA by A4;
         z = union (f.z) by A4;
        then x in union (f.z) by A18,SETFAM_1:def 1;
        then ex A0 being set st x in A0 & A0 in f.z by TARSKI:def 4;
        hence A in X by A22,A23,T_1TOPSP:def 1;
      end;
      then A in meet T by A20,SETFAM_1:def 1;
      then A in Intersect(T) by A20,CANTOR_1:def 3;
      hence thesis by A21,TARSKI:def 4;
    end;
      union B c= Intersect(F)
    proof
      let x be set;
      assume A24:x in union B;
      consider X being set such that
        A25:X in F by A1,XBOOLE_0:def 1;
A26:  f.X in T by A25;
      consider y being set such that
        A27:x in y & y in B by A24,TARSKI:def 4;
A28:  y in meet T by A26,A27,CANTOR_1:def 3;
        for X st X in F holds x in X
      proof
        let X;
        assume A29:X in F;
        then f.X in T;
        then A30:y in f.X by A28,SETFAM_1:def 1;
              X = union (f.X) by A4,A29;
       hence x in X by A27,A30,TARSKI:def 4;
      end;
      then x in meet F by A1,SETFAM_1:def 1;
      hence x in Intersect(F) by A1,CANTOR_1:def 3;
    end;
    hence thesis by A16,XBOOLE_0:def 10;
  end;
end;

theorem Th11:
for X0,X1 being Subset of Y st
   (X0 is_a_dependent_set_of PA &
    X1 is_a_dependent_set_of PA & X0 meets X1)
    holds X0 /\ X1 is_a_dependent_set_of PA
proof
  let X0,X1 be Subset of Y;
  assume A1:X0 is_a_dependent_set_of PA &
             X1 is_a_dependent_set_of PA & X0 meets X1;
  then consider A being set such that
    A2:A c= PA & A<>{} & X0 = union A by Def1;
  consider B being set such that
    A3:B c= PA & B<>{} & X1 = union B by A1,Def1;
  A4:X0 /\ X1 = union (A /\ B)
  proof
    A5:X0 /\ X1 c= union (A /\ B)
    proof
      let x be set;
      assume x in (X0 /\ X1);
      then A6:x in X0 & x in X1 by XBOOLE_0:def 3;
      then consider y being set such that
        A7:x in y & y in A by A2,TARSKI:def 4;
      consider z being set such that
        A8:x in z & z in B by A3,A6,TARSKI:def 4;
      A9:y in PA by A2,A7;
      A10:z in PA by A3,A8;
       y meets z by A7,A8,XBOOLE_0:3;
      then y = z by A9,A10,EQREL_1:def 6;
      then y in A /\ B by A7,A8,XBOOLE_0:def 3;
      hence x in union (A /\ B) by A7,TARSKI:def 4;
    end;
      union (A /\ B) c= X0 /\ X1
    proof
      let x be set;
      assume x in union (A /\ B);
      then consider y being set such that
        A11:x in y & y in (A /\ B) by TARSKI:def 4;
        y in A & y in B by A11,XBOOLE_0:def 3;
      then x in X0 & x in X1 by A2,A3,A11,TARSKI:def 4;
      hence thesis by XBOOLE_0:def 3;
    end;
    hence thesis by A5,XBOOLE_0:def 10;
  end;
  A12:A \/ B c= PA by A2,A3,XBOOLE_1:8;
  A13:A /\ B c= A by XBOOLE_1:17;
    A c= A \/ B by XBOOLE_1:7;
  then A /\ B c= A \/ B by A13,XBOOLE_1:1;
  then A14:A /\ B c= PA by A12,XBOOLE_1:1;
    now assume
A15: A /\ B={};
    consider y being set such that
      A16:y in X0 & y in X1 by A1,XBOOLE_0:3;
    thus contradiction by A4,A15,A16,XBOOLE_0:def 3,ZFMISC_1:2;
  end;
  hence thesis by A4,A14,Def1;
end;

theorem Th12:
for X being Subset of Y holds
  X is_a_dependent_set_of PA & X<>Y
  implies X` is_a_dependent_set_of PA
proof
  let X be Subset of Y;
  assume A1:X is_a_dependent_set_of PA & X<>Y;
  then consider B being set such that
    A2:B c= PA & B<>{} & X=union B by Def1;
  take PA \ B;
  A3:(union PA = Y & for A being set st A in PA holds A<>{} &
     for B being set st B in PA holds A=B or A misses B) by EQREL_1:def 6;
  then A4:X` = union PA \ union B by A2,SUBSET_1:def 5;
  reconsider B as Subset of PA by A2;
    now assume PA \ B={};
    then PA c= B by XBOOLE_1:37;
    hence contradiction by A1,A2,A3,XBOOLE_0:def 10;
  end;
  hence thesis by A4,T_1TOPSP:3,XBOOLE_1:36;
end;

theorem Th13:
for y being Element of Y
  ex X being Subset of Y st y in X & X is_min_depend PA,PB
proof
  let y be Element of Y;
  A1:(union PA = Y & for A being set st A in PA holds A<>{} &
     for B being set st B in PA holds A=B or A misses B) by EQREL_1:def 6;
  A2:Y is_a_dependent_set_of PA by Th9;
  A3:Y is_a_dependent_set_of PB by Th9;
  defpred P[set] means
   y in $1 & $1 is_a_dependent_set_of PA & $1 is_a_dependent_set_of PB;
  deffunc F(Subset of Y) = $1;
  reconsider XX={F(X) where X is Subset of Y:P[X]}
      as Subset of bool Y from SubsetFD;
  reconsider XX as Subset-Family of Y by SETFAM_1:def 7;
    Y c= Y;
then A4: Y in XX by A2,A3;
    for X1 be set st X1 in XX holds y in X1
  proof
    let X1 be set;
    assume X1 in XX;
    then consider X be Subset of Y such that
      A5:X=X1 & y in X & X is_a_dependent_set_of PA &
                       X is_a_dependent_set_of PB;
    thus thesis by A5;
  end;
then A6: y in meet XX by A4,SETFAM_1:def 1;
  then A7:Intersect(XX)<>{} by A4,CANTOR_1:def 3;
  take Intersect(XX);
    for X1 be set st X1 in XX holds X1 is_a_dependent_set_of PA
  proof
    let X1 be set;
    assume X1 in XX;
    then ex X be Subset of Y st
      X=X1 & y in X & X is_a_dependent_set_of PA &
                       X is_a_dependent_set_of PB;
    hence thesis;
  end;
  then A8:Intersect(XX) is_a_dependent_set_of PA by A7,Th10;
    for X1 be set st X1 in XX holds X1 is_a_dependent_set_of PB
  proof
    let X1 be set;
    assume X1 in XX;
    then ex X be Subset of Y st
      X=X1 & y in X &
                 X is_a_dependent_set_of PA &
                 X is_a_dependent_set_of PB;
    hence thesis;
  end;
  then A9:Intersect(XX) is_a_dependent_set_of PB by A7,Th10;
    for d being set st d c= Intersect(XX)
    & d is_a_dependent_set_of PA &
      d is_a_dependent_set_of PB holds d=Intersect(XX)
  proof
    let d be set;
    assume A10:d c= Intersect(XX) &
       d is_a_dependent_set_of PA &
       d is_a_dependent_set_of PB;
    then consider Ad being set such that
      A11:Ad c= PA & Ad<>{} & d = union Ad by Def1;
    A12:d c= Y by A1,A11,ZFMISC_1:95;
    per cases;
    suppose y in d;
     then A13:d in XX by A10,A12;
       Intersect(XX) c= d
     proof
       let X1 be set;
       assume X1 in Intersect(XX);
       then X1 in meet XX by A4,CANTOR_1:def 3;
       hence X1 in d by A13,SETFAM_1:def 1;
     end;
     hence thesis by A10,XBOOLE_0:def 10;
    suppose A14:not(y in d);
     reconsider d as Subset of Y by A1,A11,ZFMISC_1:95;
       d` = Y \ d by SUBSET_1:def 5;
     then A15:y in d` by A14,XBOOLE_0:def 4;
       d misses d` by SUBSET_1:44;
     then A16:d /\ d` = {} by XBOOLE_0:def 7;
     A17:d <> Y by A14;
     then A18:d` is_a_dependent_set_of PA by A10,Th12;
       d` is_a_dependent_set_of PB by A10,A17,Th12;
     then A19:d` in XX by A15,A18;
       Intersect(XX) c= d`
     proof
       let X1 be set;
       assume X1 in Intersect(XX);
       then X1 in meet XX by A4,CANTOR_1:def 3;
       hence X1 in d` by A19,SETFAM_1:def 1;
     end;
     then d /\ Intersect(XX) c= {} by A16,XBOOLE_1:26;
     then A20:d /\ Intersect(XX) = {} by XBOOLE_1:3;
      d /\ d c= d /\ Intersect(XX) by A10,XBOOLE_1:26;
     then A21:union Ad = {} by A11,A20,XBOOLE_1:3;
     consider ad being set such that
       A22:ad in Ad by A11,XBOOLE_0:def 1;
     A23:ad<>{} by A1,A11,A22;
     A24:ad c= {} by A21,A22,ZFMISC_1:92;
       ex add being set st add in ad by A23,XBOOLE_0:def 1;
     hence thesis by A24;
  end;
  hence thesis by A4,A6,A8,A9,Def2,CANTOR_1:def 3;
end;

theorem Th14: for P being a_partition of Y
  for y being Element of Y
   ex A being Subset of Y st y in A & A in P
proof
  let P be a_partition of Y;
  let y be Element of Y;
  consider R being Equivalence_Relation of Y such that
   A1: P = Class R by EQREL_1:43;
  take Class(R,y);
  thus y in Class(R,y) by EQREL_1:28;
  thus Class(R,y) in P by A1,EQREL_1:def 5;
end;

definition
 let Y be non empty set;
 cluster -> non empty a_partition of Y;
 coherence
 proof
   let P be a_partition of Y;
   consider y being Element of Y;
   consider A being Subset of Y such that A1:y in A & A in P by Th14;
   thus P is non empty by A1;
 end;
end;

definition let Y be set;
func PARTITIONS(Y) means
:Def3: for x being set holds x in it iff x is a_partition of Y;
existence
proof
  defpred P[set] means $1 is a_partition of Y;
  consider X being set such that
  A1:for x being set holds x in X iff x in bool bool Y & P[x] from Separation;
  take X;
  let x be set;
  thus x in X implies x is a_partition of Y by A1;
  assume
    x is a_partition of Y;
  hence x in X by A1;
end;
uniqueness
proof
  let A1,A2 be set such that
  A2: for x being set holds x in A1 iff x is a_partition of Y and
  A3: for x being set holds x in A2 iff x is a_partition of Y;
    now let y be set;
    y in A1 iff y is a_partition of Y by A2;
  hence y in A1 iff y in A2 by A3;
  end;
  hence A1=A2 by TARSKI:2;
end;
end;

definition
let Y be set;
cluster PARTITIONS(Y) -> non empty;
coherence
proof
  per cases;
  suppose A1:Y={};
     {} c= bool {} by XBOOLE_1:2;
   then {} is Subset-Family of {} by SETFAM_1:def 7;
   then {} is a_partition of Y by A1,EQREL_1:def 6;
  hence thesis by Def3;
  suppose Y<>{};
   then reconsider Y as non empty set;
     {Y} c= bool Y by ZFMISC_1:80;
   then A2:{Y} is Subset-Family of Y by SETFAM_1:def 7;
   A3:union {Y} = Y by ZFMISC_1:31;
     for A being Subset of Y st A in {Y} holds A<>{} &
   for B being Subset of Y st B in {Y} holds A = B or A misses B
   proof
     let A be Subset of Y;
     assume A4: A in {Y};
     then A5:A=Y by TARSKI:def 1;
     thus A<>{} by A4,TARSKI:def 1;
     let B be Subset of Y;
     assume B in {Y};
     hence thesis by A5,TARSKI:def 1;
   end;
   then {Y} is a_partition of Y by A2,A3,EQREL_1:def 6;
  hence thesis by Def3;
end;
end;

begin

::Chap. 2  Join and Meet Operation between Partitions

definition let Y;let PA,PB be a_partition of Y;
 func PA '/\' PB -> a_partition of Y equals
 :Def4: INTERSECTION(PA,PB) \ {{}};
correctness
proof
     {} c= Y by XBOOLE_1:2;
   then {{}} c= bool Y by ZFMISC_1:37;
   then reconsider e = {{}} as Subset-Family of Y by SETFAM_1:def 7;
   set a = INTERSECTION(PA,PB);
     a c= bool Y
   proof
       for z being set st z in a holds
         z in bool Y
     proof
       let z be set;
       assume z in a;
       then ex M,N being set st M in PA & N in PB & z = M /\ N by SETFAM_1:def
5;
       then z c= Y by XBOOLE_1:108;
       hence thesis;
     end;
     hence thesis by TARSKI:def 3;
   end;
   then reconsider a = INTERSECTION(PA,PB) as Subset-Family of Y by SETFAM_1:
def 7;
   reconsider ia = a \ e as Subset-Family of Y by SETFAM_1:def 7;
   A1: union PA = Y & union PB = Y by EQREL_1:def 6;
   A2: union ia = union INTERSECTION(PA,PB) by Th3
                .= union PA /\ union PB by LATTICE4:2
                .= Y by A1;
     for A being Subset of Y st A in ia holds A<>{} &
      for B being Subset of Y st B in ia
      holds A = B or A misses B
   proof
     let A be Subset of Y;
     assume A3: A in ia;
     then A4: not A in {{}} by XBOOLE_0:def 4;
     A5: A in INTERSECTION(PA,PB) by A3,XBOOLE_0:def 4;
       for B being Subset of Y st B in ia
     holds A = B or A misses B
     proof
       A6:for m,n,o,p being set holds
           (m /\ n) /\ (o /\ p) = m /\ ( n /\ o /\ p)
       proof
         let m,n,o,p be set;
           (m /\ n) /\ (o /\ p) = m /\ ( n /\ (o /\ p) ) by XBOOLE_1:16
                          .= m /\ ( n /\ o /\ p) by XBOOLE_1:16;
         hence thesis;
       end;
       let B be Subset of Y;
       assume B in ia;
       then B in INTERSECTION(PA,PB) by XBOOLE_0:def 4;
       then consider M,N being set such that
       A7: M in PA and
       A8: N in PB and
       A9: B = M /\ N by SETFAM_1:def 5;
       consider S,T being set such that
       A10: S in PA and
       A11: T in PB and
       A12: A = S /\ T by A5,SETFAM_1:def 5;
         (M /\ N = S /\ T) or (not ( M = S) or not ( N = T ));
       then (M /\ N = S /\ T) or (M misses S or N misses T)
             by A7,A8,A10,A11,EQREL_1:def 6;
       then A13: (M /\ N = S /\ T) or ( M /\ S = {} or N /\ T = {})
             by XBOOLE_0:def 7;
         (M /\ S) /\ (N /\ T) = M /\ ( S /\ N /\ T ) by A6
                        .=( M /\ N ) /\ ( S /\ T ) by A6;
       hence thesis by A9,A12,A13,XBOOLE_0:def 7;
     end;
     hence thesis by A4,TARSKI:def 1;
   end;
   hence thesis by A2,EQREL_1:def 6;
 end;
commutativity;
end;

theorem for PA being a_partition of Y holds
  PA '/\' PA = PA
proof
  let PA be a_partition of Y;
  A1: PA '/\' PA = INTERSECTION(PA,PA) \ {{}} by Def4;
  A2: INTERSECTION(PA,PA) \ {{}} '<' PA
  proof
      for u being set st u in INTERSECTION(PA,PA) \ {{}} ex v being set
         st v in PA & u c= v
    proof
      let u be set;
      assume u in INTERSECTION(PA,PA) \ {{}};
      then u in INTERSECTION(PA,PA) by XBOOLE_0:def 4;
      then consider v,u2 being set such that
      A3: v in PA and
        u2 in PA and
      A4: u = v /\ u2 by SETFAM_1:def 5;
      take v;
      thus thesis by A3,A4,XBOOLE_1:17;
    end;
    hence thesis by SETFAM_1:def 2;
  end;
    PA '<' INTERSECTION(PA,PA) \ {{}}
  proof
      for u being set st u in PA
      ex v being set st v in INTERSECTION(PA,PA) \ {{}} & u c= v
    proof let u be set;
      assume A5: u in PA;
      then A6: u <> {} by EQREL_1:def 6;
      set v = u /\ u;
      A7: not v in {{}} by A6,TARSKI:def 1;
        v in INTERSECTION(PA,PA) by A5,SETFAM_1:def 5;
      then v in INTERSECTION(PA,PA) \ {{}} by A7,XBOOLE_0:def 4;
      hence thesis;
    end;
    hence thesis by SETFAM_1:def 2;
  end;
  hence thesis by A1,A2,Th5;
end;

theorem for PA,PB,PC being a_partition of Y holds
  (PA '/\' PB) '/\' PC = PA '/\' (PB '/\' PC)
proof
  let PA ,PB ,PC  be a_partition of Y;
  consider PD,PE being a_partition of Y such that
  A1: PD = PA '/\' PB and
  A2: PE = PB '/\' PC;
  A3: PD '/\' PC '<' PA '/\' PE
  proof
      for u being set st u in PD '/\' PC
    ex v being set st v in PA '/\' PE & u c= v
    proof
      let u be set;
      assume u in PD '/\' PC;
      then A4: u in INTERSECTION(PD,PC) \ {{}} by Def4;
      then u in INTERSECTION(PD,PC) by XBOOLE_0:def 4;
      then consider u1, u2 being set such that
      A5: u1 in PD and
      A6: u2 in PC and
      A7: u = u1 /\ u2 by SETFAM_1:def 5;
        u1 in INTERSECTION(PA,PB) \ {{}} by A1,A5,Def4;
      then u1 in INTERSECTION(PA,PB) by XBOOLE_0:def 4;
      then consider u3, u4 being set such that
      A8: u3 in PA and
      A9: u4 in PB and
      A10: u1 = u3 /\ u4 by SETFAM_1:def 5;
      consider v, v1,v2 being set such that
      A11: v1 = u4 /\ u2 and
      A12: v2 = u3 and
      A13: v = u3 /\ u4 /\ u2;
      A14: v = v2 /\ v1 by A11,A12,A13,XBOOLE_1:16;
      A15: v1 in INTERSECTION(PB,PC) by A6,A9,A11,SETFAM_1:def 5;
      A16: not u in {{}} by A4,XBOOLE_0:def 4;
        u = u3 /\ v1 by A7,A10,A11,XBOOLE_1:16;
      then v1 <> {} by A16,TARSKI:def 1;
      then not v1 in {{}} by TARSKI:def 1;
      then v1 in INTERSECTION(PB,PC) \ {{}} by A15,XBOOLE_0:def 4;
      then v1 in PE by A2,Def4;
      then v in INTERSECTION(PA,PE) by A8,A12,A14,SETFAM_1:def 5;
then A17:  v in INTERSECTION(PA,PE) \ {{}} by A7,A10,A13,A16,XBOOLE_0:def 4;
      take v;
      thus thesis by A7,A10,A13,A17,Def4;
    end;
    hence thesis by SETFAM_1:def 2;
  end;
    PA '/\' PE '<' PD '/\' PC
  proof
      for u being set st u in PA '/\' PE
    ex v being set st v in PD '/\' PC & u c= v
    proof
      let u be set;
      assume u in PA '/\' PE;
      then A18: u in INTERSECTION(PA,PE) \ {{}} by Def4;
      then u in INTERSECTION(PA,PE) by XBOOLE_0:def 4;
      then consider u1,u2 being set such that
      A19: u1 in PA and
      A20: u2 in PE and
      A21: u = u1 /\ u2 by SETFAM_1:def 5;
        u2 in INTERSECTION(PB,PC) \ {{}} by A2,A20,Def4;
      then u2 in INTERSECTION(PB,PC) by XBOOLE_0:def 4;
      then consider u3,u4 being set such that
      A22: u3 in PB and
      A23: u4 in PC and
      A24: u2 = u3 /\ u4 by SETFAM_1:def 5;
      A25: u = u1 /\ u3 /\ u4 by A21,A24,XBOOLE_1:16;
      consider v, v1,v2 being set such that
      A26: v1 = u1 /\ u3 and
        v2 = u4 and
      A27: v = u1 /\ u3 /\ u4;
      A28: v1 in INTERSECTION(PA,PB) by A19,A22,A26,SETFAM_1:def 5;
      A29: not u in {{}} by A18,XBOOLE_0:def 4;
      then v1 <> {} by A25,A26,TARSKI:def 1;
      then not v1 in {{}} by TARSKI:def 1;
      then v1 in INTERSECTION(PA,PB) \ {{}} by A28,XBOOLE_0:def 4;
      then v1 in PD by A1,Def4;
      then v in INTERSECTION(PD,PC) by A23,A26,A27,SETFAM_1:def 5;
      then A30: v in INTERSECTION(PD,PC) \ {{}} by A25,A27,A29,XBOOLE_0:def 4;
      take v;
      thus thesis by A21,A24,A27,A30,Def4,XBOOLE_1:16;
    end;
    hence thesis by SETFAM_1:def 2;
  end;
  hence thesis by A1,A2,A3,Th5;
end;

theorem Th17: for PA,PB being a_partition of Y holds
  PA '>' PA '/\' PB
proof
  let PA,PB be a_partition of Y;
  thus PA '>' PA '/\' PB
  proof
      for u being set st u in PA '/\' PB
    ex v being set st v in PA & u c= v
    proof
      let u be set;
      assume u in PA '/\' PB;
      then u in INTERSECTION(PA,PB)\ {{}} by Def4;
      then u in INTERSECTION(PA,PB) by XBOOLE_0:def 4;
      then consider u1,u2 being set such that
      A1: u1 in PA and
        u2 in PB and
      A2: u = u1 /\ u2 by SETFAM_1:def 5;
      take u1;
      thus thesis by A1,A2,XBOOLE_1:17;
    end;
    hence thesis by SETFAM_1:def 2;
  end;
end;

definition let Y;let PA,PB be a_partition of Y;
 func PA '\/' PB -> a_partition of Y means
 :Def5: for d holds d in it iff d is_min_depend PA,PB;
existence
proof
   A1:(union PA = Y & for A being set st A in PA holds A<>{} &
     for B being set st B in PA holds A=B or A misses B) by EQREL_1:def 6;
   defpred P[set] means $1 is_min_depend PA,PB;
   consider X being set such that
    A2:for d being set holds d in X iff d in bool Y & P[d] from Separation;
   A3:for d being set holds (d in X) iff (d is_min_depend PA,PB)
   proof
     let d be set;
       for d being set holds (d is_min_depend PA,PB) implies (d in bool Y)
     proof
       let d be set;
       assume d is_min_depend PA,PB;
       then d is_a_dependent_set_of PA &
           d is_a_dependent_set_of PB &
       for x being set st x c= d
         & x is_a_dependent_set_of PA &
           x is_a_dependent_set_of PB holds x=d by Def2;
       then consider A being set such that
         A4:A c= PA & A<>{} & d = union A by Def1;
         d c= union PA by A4,ZFMISC_1:95;
       hence d in bool Y by A1;
     end;
        then (d is_min_depend PA,PB) implies
         (d is_min_depend PA,PB) & (d in bool Y);
     hence thesis by A2;
   end;
   take X;
   A5:union X = Y
   proof
     A6:Y c= union X
     proof
       let y be set;
       assume y in Y;
       then consider a being Subset of Y such that
         A7:y in a & a is_min_depend PA,PB by Th13;
         a in X by A3,A7;
       hence thesis by A7,TARSKI:def 4;
     end;
       union X c= Y
     proof
       let y be set;
       assume y in union X;
       then consider a being set such that
         A8:y in a & a in X by TARSKI:def 4;
         a is_min_depend PA,PB by A3,A8;
       then a is_a_dependent_set_of PA &
       a is_a_dependent_set_of PB &
       for d being set st d c= a &
           d is_a_dependent_set_of PA &
           d is_a_dependent_set_of PB holds d=a by Def2;
       then consider A being set such that
         A9: A c= PA & A<>{} & a = union A by Def1;
         a c= Y by A1,A9,ZFMISC_1:95;
       hence y in Y by A8;
     end;
     hence thesis by A6,XBOOLE_0:def 10;
   end;
   A10:for A being Subset of Y st A in X holds A<>{} &
   for B being Subset of Y st B in X holds A=B or A misses B
   proof
     let A be Subset of Y;
     assume A in X;
  then A11: A is_min_depend PA,PB by A3;
then A12: A is_a_dependent_set_of PA &
     A is_a_dependent_set_of PB &
     for d being set st d c= A &
         d is_a_dependent_set_of PA &
         d is_a_dependent_set_of PB holds d=A by Def2;
     then consider Aa being set such that
A13:   Aa c= PA & Aa<>{} & A = union Aa by Def1;
     consider aa being set such that
       A14:aa in Aa by A13,XBOOLE_0:def 1;
     A15:aa<>{} by A1,A13,A14;
     A16:aa c= union Aa by A14,ZFMISC_1:92;
       ex ax being set st ax in aa by A15,XBOOLE_0:def 1;
     hence A<>{} by A13,A16;
     let B be Subset of Y;
     assume B in X;
  then A17: B is_min_depend PA,PB by A3;
then A18: B is_a_dependent_set_of PA &
     B is_a_dependent_set_of PB &
     for d being set st d c= B &
         d is_a_dependent_set_of PA &
         d is_a_dependent_set_of PB holds d=B by Def2;
       now assume A19:A meets B;
       then A20:A /\ B is_a_dependent_set_of PA by A12,A18,Th11;
       A21:A /\ B is_a_dependent_set_of PB by A12,A18,A19,Th11;
         A /\ B c= A by XBOOLE_1:17;
       then A22:A /\ B = A by A11,A20,A21,Def2;
       A23:A c= B
       proof
         let x be set;
         assume x in A;
         hence x in B by A22,XBOOLE_0:def 3;
       end;
         A /\ B c= B by XBOOLE_1:17;
       then A24:A /\ B = B by A17,A20,A21,Def2;
         B c= A
       proof
         let x be set;
         assume x in B;
         hence x in A by A24,XBOOLE_0:def 3;
       end;
       hence A=B by A23,XBOOLE_0:def 10;
     end;
     hence thesis;
   end;
     X c= bool Y
   proof
     let x be set;
     assume x in X;
     then x is_min_depend PA,PB by A3;
     then x is_a_dependent_set_of PA &
     x is_a_dependent_set_of PB &
     for d being set st d c= x &
         d is_a_dependent_set_of PA &
         d is_a_dependent_set_of PB holds d=x by Def2;
     then consider a being set such that
A25:   a c= PA & a<>{} & x = union a by Def1;
       x c= Y by A1,A25,ZFMISC_1:95;
     hence thesis;
   end;
   then reconsider X as Subset-Family of Y by SETFAM_1:def 7;
     X is a_partition of Y by A5,A10,EQREL_1:def 6;
   hence thesis by A3;
end;
uniqueness
proof
  let A1,A2 be a_partition of Y such that
  A26: for x being set holds x in A1 iff x is_min_depend PA,PB and
  A27: for x being set holds x in A2 iff x is_min_depend PA,PB;
    now let y be set;
      y in A1 iff y is_min_depend PA,PB by A26;
    hence y in A1 iff y in A2 by A27;
  end;
  hence A1=A2 by TARSKI:2;
end;
commutativity
proof
  let IT,PA,PB be a_partition of Y;
  A28:now let a be set;
     assume a is_min_depend PA,PB;
    then a is_a_dependent_set_of PB &
    a is_a_dependent_set_of PA & for d being set st d c= a
    & d is_a_dependent_set_of PB &
    d is_a_dependent_set_of PA holds d=a by Def2;
    hence a is_min_depend PB,PA by Def2;
  end;
  A29:now let a be set;
     assume a is_min_depend PB,PA;
    then a is_a_dependent_set_of PA &
    a is_a_dependent_set_of PB & for d being set st d c= a
    & d is_a_dependent_set_of PA &
    d is_a_dependent_set_of PB holds d=a by Def2;
    hence a is_min_depend PA,PB by Def2;
  end;
     (for d being set holds (d in a) iff (d is_min_depend PA,PB))
    implies
   (for d being set holds (d in a) iff (d is_min_depend PB,PA))
   proof assume
A30:for d being set holds (d in a) iff (d is_min_depend PA,PB);
    let d be set;
A31:   d in a iff d is_min_depend PA,PB by A30;
    hence d in a implies d is_min_depend PB,PA by A28;
    assume d is_min_depend PB,PA;
    hence d in a by A29,A31;
   end;
  hence thesis;
end;
end;

canceled;

theorem Th19: for PA,PB being a_partition of Y holds
  PA '<' PA '\/' PB
proof
  thus PA '<' PA '\/' PB
  proof
      for a being set st a in PA ex b being set
    st b in PA '\/' PB & a c= b
    proof
      let a be set;
      assume A1: a in PA;
      then A2: a c= Y & a<>{} by EQREL_1:def 6;
      consider x being Element of a;
      A3: x in Y by A2,TARSKI:def 3;
        union (PA '\/' PB) = Y by EQREL_1:def 6;
      then consider b being set such that
      A4: x in b & b in PA '\/' PB by A3,TARSKI:def 4;
        b is_min_depend PA,PB by A4,Def5;
      then b is_a_dependent_set_of PA by Def2;
      then consider B being set such that A5:B c= PA & B<>{} & b = union B by
Def1;
        a in B
      proof
        consider u being set such that
        A6: x in u & u in B by A4,A5,TARSKI:def 4;
          a /\ u <> {} by A2,A6,XBOOLE_0:def 3;
        then A7: not (a misses u) by XBOOLE_0:def 7;
          u in PA by A5,A6;
        hence thesis by A1,A6,A7,EQREL_1:def 6;
      end;
      then a c= b by A5,ZFMISC_1:92;
      hence thesis by A4;
    end;
    hence thesis by SETFAM_1:def 2;
  end;
end;

theorem for PA being a_partition of Y holds
  PA '\/' PA = PA
proof
  let PA be a_partition of Y;
  A1:PA '<' PA '\/' PA by Th19;
    PA '\/' PA '<' PA
  proof
      for a being set st a in PA '\/' PA ex b being set st b in PA & a c= b
    proof
      let a be set;
      assume A2: a in PA '\/' PA;
      then A3: a is_min_depend PA,PA by Def5;
      then a is_a_dependent_set_of PA &
      for d being set st d c= a &
      d is_a_dependent_set_of PA holds d=a by Def2;
      then consider B being set such that
      A4:B c= PA & B<>{} & a = union B by Def1;
      A5: a c= Y & a <> {} by A2,EQREL_1:def 6;
      consider x being Element of a;
         x in a by A5;
      then x in Y by A2;
      then x in union PA by EQREL_1:def 6;
      then consider b being set such that A6: x in b & b in PA by TARSKI:def 4;
        b in B
      proof
        consider u being set such that
        A7: x in u & u in B by A4,A5,TARSKI:def 4;
          b /\ u <> {} by A6,A7,XBOOLE_0:def 3;
        then A8: not (b misses u) by XBOOLE_0:def 7;
          u in PA by A4,A7;
        hence thesis by A6,A7,A8,EQREL_1:def 6;
      end;
      then A9:b c= a by A4,ZFMISC_1:92;
        b is_a_dependent_set_of PA by A6,Th8;
      then a = b by A3,A9,Def2;
      hence thesis by A6;
    end;
    hence thesis by SETFAM_1:def 2;
  end;
  hence thesis by A1,Th5;
end;

theorem Th21: for PA,PC being a_partition of Y st
  PA '<' PC & x in PC & z0 in PA & t in x & t in z0 holds z0 c= x
proof
  let PA,PC be a_partition of Y;
  assume A1:PA '<' PC & x in PC & z0 in PA & t in x & t in z0;
  then consider b such that A2:b in PC & z0 c= b by SETFAM_1:def 2;
    x = b or x misses b by A1,A2,EQREL_1:def 6;
  hence z0 c= x by A1,A2,XBOOLE_0:3;
end;

theorem for PA,PB being a_partition of Y st
  x in (PA '\/' PB) & z0 in PA & t in x & t in z0 holds z0 c= x
proof
  let PA,PB be a_partition of Y;
  assume A1:x in (PA '\/' PB) & z0 in PA & t in x & t in z0;
    PA '<' PA '\/' PB by Th19;
  hence z0 c= x by A1,Th21;
end;

begin

::Chap. 3  Partitions and Equivalence Relations

theorem Th23: for PA being a_partition of Y
  ex RA being Equivalence_Relation of Y st
     for x,y holds [x,y] in RA iff ex A st A in PA & x in A & y in A
proof let PA be a_partition of Y;
  A1: union PA = Y & for A st A in PA holds A<>{} &
      for B st B in PA holds A = B or A misses B by EQREL_1:def 6;
    ex RA being Equivalence_Relation of Y st
     for x,y holds [x,y] in RA iff ex A st A in PA & x in A & y in A
  proof
    defpred P[set,set] means ex A st A in PA & $1 in A & $2 in A;
    A2: for x st x in Y holds P[x,x]
    proof
      let x;
      assume x in Y;
      then ex Z being set st x in Z & Z in PA by A1,TARSKI:def 4;
      then consider Z such that A3: x in Z & Z in PA;
      reconsider A = Z as Subset of Y by A3;
      take A;
      thus thesis by A3;
    end;
    A4: for x,y st P[x,y] holds P[y,x];
    A5: for x,y,z st P[x,y] & P[y,z] holds P[x,z]
    proof let x,y,z;
      given A such that A6: A in PA & x in A & y in A;
      given B such that A7: B in PA & y in B & z in B;
         A = B or A misses B by A6,A7,EQREL_1:def 6;
      hence thesis by A6,A7,XBOOLE_0:3;
    end;
    consider RA being Equivalence_Relation of Y such that
     A8: for x,y holds [x,y] in RA iff
      x in Y & y in Y & P[x,y] from Ex_Eq_Rel(A2,A4,A5);
    take RA;
    thus thesis by A8;
  end;
  hence thesis;
end;

definition let Y; let PA be a_partition of Y;
 func ERl PA -> Equivalence_Relation of Y means
:Def6:  for x1,x2 being set holds
   [x1,x2] in it iff ex A st A in PA & x1 in A & x2 in A;
existence by Th23;
uniqueness
proof
   let f1,f2 be Equivalence_Relation of Y such that
A1: for x1,x2 being set holds [x1,x2] in f1 iff
    ex A st A in PA & x1 in A & x2 in A and
A2: for x1,x2 being set holds [x1,x2] in f2 iff
    ex A st A in PA & x1 in A & x2 in A;
   let x1,x2 be set;
      [x1,x2] in f1 iff ex A st A in PA & x1 in A & x2 in A by A1;
   hence thesis by A2;
 end;
end;

definition let Y;
 defpred P[set,set] means ex PA st PA = $1 & $2 = ERl PA;
A1: for x st x in PARTITIONS(Y) ex z st P[x,z]
  proof let x;
   assume x in PARTITIONS(Y);
    then reconsider x as a_partition of Y by Def3;
   take ERl x;
   thus thesis;
  end;
 func Rel(Y) -> Function means
     dom it = PARTITIONS(Y) &
   for x st x in PARTITIONS(Y) ex PA st PA = x & it.x = ERl PA;
existence
 proof
  thus ex f being Function st dom f = PARTITIONS(Y)
    & for x st x in PARTITIONS(Y) holds P[x,f.x] from NonUniqFuncEx(A1);
 end;
uniqueness
proof
   let f1,f2 be Function such that
A2: dom f1 = PARTITIONS(Y) and
A3: for x st x in PARTITIONS(Y) ex PA st PA = x & f1.x = ERl PA and
A4: dom f2 = PARTITIONS(Y) and
A5: for x st x in PARTITIONS(Y) ex PA st PA = x & f2.x = ERl PA;
     for z st z in PARTITIONS(Y) holds f1.z = f2.z
   proof
     let x;
     assume A6: x in PARTITIONS(Y);
      then A7:     ex PA st PA = x & f1.x = ERl PA by A3;
        ex PA st PA = x & f2.x = ERl PA by A5,A6;
     hence thesis by A7;
   end;
   hence thesis by A2,A4,FUNCT_1:9;
 end;
end;

theorem Th24: for PA,PB being a_partition of Y holds
  PA '<' PB iff ERl(PA) c= ERl(PB)
proof
  let PA,PB be a_partition of Y;
  set RA = ERl PA, RB = ERl PB;

  hereby assume A1: PA '<' PB;
      for x1,x2 being set holds [x1,x2] in RA implies [x1,x2] in RB
    proof let x1,x2 be set;
      assume [x1,x2] in RA;
       then consider A being Subset of Y such that
A2:    A in PA & x1 in A & x2 in A by Def6;
        (ex y st y in PB & A c= y) by A1,A2,SETFAM_1:def 2;
      hence thesis by A2,Def6;
    end;
    hence ERl(PA) c= ERl(PB) by RELAT_1:def 3;
  end;
  assume A3: ERl(PA) c= ERl(PB);
    for x st x in PA ex y st y in PB & x c= y
  proof
    let x;
    assume A4:x in PA;
    then A5:x<>{} by EQREL_1:def 6;
    consider x0 being Element of x;
    set y={z where z is Element of Y:[x0,z] in ERl(PB)};
    A6:x c= y
    proof
      let x1;
      assume A7: x1 in x;
      then [x0,x1] in RA by A4,Def6;
     hence x1 in y by A3,A4,A7;
    end;
    consider x1 being Element of x;
      [x0,x1] in RA by A4,A5,Def6;
    then consider B being Subset of Y such that
      A8:B in PB & x0 in B & x1 in B by A3,Def6;
      y=B
    proof
      A9:y c= B
      proof
        let x2;
        assume x2 in y;
        then consider z being Element of Y such that
          A10:z=x2 & ([x0,z] in ERl(PB));
        consider B2 being Subset of Y such that
          A11:B2 in PB & x0 in B2 & x2 in B2 by A10,Def6;
          B2 meets B by A8,A11,XBOOLE_0:3;
        hence x2 in B by A8,A11,EQREL_1:def 6;
      end;
        B c= y
      proof
        let x2;
        assume A12: x2 in B;
        then [x0,x2] in RB by A8,Def6;
        hence thesis by A12;
      end;
      hence y=B by A9,XBOOLE_0:def 10;
    end;
    hence ex y st y in PB & x c= y by A6,A8;
  end;
  hence PA '<' PB by SETFAM_1:def 2;
end;

theorem Th25: for PA,PB being a_partition of Y,p0,x,y being set,
f being FinSequence of Y st p0 c= Y &
x in p0 & f.1=x & f.len f=y & 1 <= len f &
(for i st 1<=i & i<len f
ex p2,p3,u being set st p2 in PA & p3 in PB &
  f.i in p2 & u in p2 & u in p3 & f.(i+1) in p3) &
p0 is_a_dependent_set_of PA &
p0 is_a_dependent_set_of PB holds
y in p0
proof
  let PA,PB be a_partition of Y,
      p0,x,y be set,
      f be FinSequence of Y;
  assume A1:p0 c= Y &
    x in p0 & f.1=x & f.len f=y & 1 <= len f &
    (for i st 1<=i & i<len f
     ex p2,p3,u being set st
       p2 in PA & p3 in PB & f.i in p2 & u in p2 & u in p3 & f.(i+1) in p3) &
    p0 is_a_dependent_set_of PA &
    p0 is_a_dependent_set_of PB;
  then consider A1 being set such that
    A2:A1 c= PA & A1<>{} & p0 = union A1 by Def1;
  consider B1 being set such that
    A3:B1 c= PB & B1<>{} & p0 = union B1 by A1,Def1;
  A4:(union PA = Y & for A being set st A in PA holds A<>{} &
    for B being set st B in PA holds A=B or A misses B) by EQREL_1:def 6;
  A5:(union PB = Y & for A being set st A in PB holds A<>{} &
    for B being set st B in PB holds A=B or A misses B) by EQREL_1:def 6;
    for k st 1 <= k & k <= len f holds f.k in p0
  proof
    defpred P[Nat] means 1 <= $1 & $1 <= len f implies f.$1 in p0;
    A6: P[0];
    A7: for k st P[k] holds P[k+1]
    proof let k;
      assume A8: P[k];
      assume A9: 1<=k+1 & k+1<=len f;
      then A10: k < len f by NAT_1:38;
        1 <= k or 1 = k + 1 by A9,NAT_1:26;
      then A11: 1 <= k or 1 - 1 = k by XCMPLX_1:26;
        now per cases by A11;
       suppose A12:1 <= k;
        then consider p2,p3,u being set such that
A13:p2 in PA & p3 in PB & f.k in p2 & u in p2 &
       u in p3 & f.(k+1) in p3 by A1,A10;
        consider A being set such that
          A14:f.k in A & A in PA by A1,A4,A8,A9,A12,NAT_1:38,TARSKI:def 4;
        A15: p2=A or p2 misses A by A13,A14,EQREL_1:def 6;
        consider a being set such that
          A16:f.k in a & a in A1 by A2,A8,A9,A12,NAT_1:38,TARSKI:def 4;
          a=p2 or a misses p2 by A2,A4,A13,A16;
        then A17: A c= p0 by A2,A13,A14,A15,A16,XBOOLE_0:3,ZFMISC_1:92;
        consider B being set such that
          A18:u in B & B in PB by A13;
        A19: p3=B or p3 misses B by A13,A18,EQREL_1:def 6;
        consider b being set such that
          A20:u in b & b in B1 by A3,A13,A14,A15,A17,TARSKI:def 4,XBOOLE_0:3;
          p3=b or p3 misses b by A3,A5,A13,A20;
        then B c= p0 by A3,A13,A18,A19,A20,XBOOLE_0:3,ZFMISC_1:92;
        hence f.(k+1) in p0 by A13,A18,A19,XBOOLE_0:3;
       suppose 0 = k;
        hence f.(k+1) in p0 by A1;
      end;
      hence f.(k+1) in p0;
    end;
    thus P[k] from Ind(A6,A7);
  end;
  hence y in p0 by A1;
end;

theorem Th26:
for R1,R2 being Equivalence_Relation of Y,f being FinSequence of Y,
  x,y being set st x in Y & y in Y & f.1=x & f.len f=y & 1 <= len f &
   (for i st 1<=i & i<len f
    ex u being set st u in Y & [f.i,u] in (R1 \/ R2) & [u,f.(i+1)] in (R1 \/
 R2))
    holds [x,y] in (R1 "\/" R2)
proof
  let R1,R2 be Equivalence_Relation of Y,f be FinSequence of Y,
  x,y be set;
  assume A1:x in Y & y in Y & f.1=x & f.len f=y & 1 <= len f &
   (for i st 1<=i & i<len f
    ex u being set st u in Y & [f.i,u] in R1 \/ R2 & [u,f.(i+1)] in R1 \/ R2);
    for i st 1 <= i & i <= len f holds [f.1,f.i] in (R1 "\/" R2)
  proof
    defpred P[Nat] means 1<=$1 & $1<=len f implies [f.1,f.$1] in R1 "\/" R2;
    A2: P[0];
    A3: for i st P[i] holds P[i+1]
    proof let i;
      assume A4: P[i];
      assume A5: 1 <= i + 1 & i + 1 <= len f;
      then A6: i < len f by NAT_1:38;
        1 <= i or 1 = i + 1 by A5,NAT_1:26;
      then A7:1 <= i or 1 - 1 = i by XCMPLX_1:26;
      A8: R1 \/ R2 c= R1 "\/" R2 by EQREL_1:def 3;
        now per cases by A7;
        suppose A9: 1 <= i;
         then consider u being set such that
     A10:u in Y & [f.i,u] in R1 \/ R2 & [u,f.(i+1)] in R1 \/ R2 by A1,A6;
         reconsider u as Element of Y by A10;
         A11:dom f = Seg len f by FINSEQ_1:def 3;
         then i in dom f by A6,A9,FINSEQ_1:3;
         then reconsider f1=f.i as Element of Y by FINSEQ_2:13;
           (i+1) in dom f by A5,A11,FINSEQ_1:3;
         then reconsider f2=f.(i+1) as Element of Y by FINSEQ_2:13;
         reconsider p = <*f1,u,f2*> as FinSequence of Y;
         A12:len p = 3 & p.1 = f.i & p.2 = u & p.3 = f.(i+1) by FINSEQ_1:62;
           for j st 1 <= j & j < len p holds [p.j,p.(j+1)] in (R1 \/ R2)
         proof
           let j;
           assume 1 <= j & j < len p;
           then 1 <= j & j < 2+1 by FINSEQ_1:62;
           then 1 <= j & j <= 2 by NAT_1:38;
           then 1 <= j & (j = 0 or j = 1 or j = 2) by CQC_THE1:3;
           hence [p.j,p.(j+1)] in (R1 \/ R2) by A10,A12;
         end;
         then [f.i,f.(i+1)] in R1 "\/" R2 by A12,EQREL_1:36;
         hence [f.1,f.(i+1)] in R1 "\/" R2 by A4,A5,A9,EQREL_1:13,NAT_1:38;
        suppose A13: 0 = i;
           [f.1,f.1] in R1 by A1,EQREL_1:11;
         then [f.1,f.1] in R1 \/ R2 by XBOOLE_0:def 2;
         hence [f.1,f.(i+1)] in R1 "\/" R2 by A8,A13;
       end;
     hence [f.1,f.(i+1)] in R1 "\/" R2;
    end;
    thus P[i] from Ind(A2,A3);
  end;
  hence thesis by A1;
end;

theorem Th27: for PA,PB being a_partition of Y holds
  ERl(PA '\/' PB) = ERl(PA) "\/" ERl(PB)
proof
  let PA,PB be a_partition of Y;
  A1: PA is_finer_than (PA '\/' PB) by Th19;
  A2: PB is_finer_than (PA '\/' PB) by Th19;
  A3:(union PA = Y & for A being set st A in PA holds A<>{} &
    for B being set st B in PA holds A=B or A misses B) by EQREL_1:def 6;
  A4:(union PB = Y & for A being set st A in PB holds A<>{} &
    for B being set st B in PB holds A=B or A misses B) by EQREL_1:def 6;
  A5:ERl(PA '\/' PB) c= (ERl(PA) "\/" ERl(PB))
  proof
    let x,y be set;
    assume [x,y] in ERl(PA '\/' PB);
    then consider p0 being Subset of Y such that
      A6:p0 in (PA '\/' PB) & x in p0 & y in p0 by Def6;
    A7: p0 is_min_depend PA,PB by A6,Def5;
    then A8:p0 is_a_dependent_set_of PA &
       p0 is_a_dependent_set_of PB &
       for d being set st d c= p0
         & d is_a_dependent_set_of PA &
           d is_a_dependent_set_of PB holds d=p0 by Def2;
    then consider A1 being set such that
      A9:A1 c= PA & A1<>{} & p0 = union A1 by Def1;
    consider a being set such that A10:x in a & a in A1 by A6,A9,TARSKI:def 4;
    reconsider Ca={ p where p is Element of PA:
      ex f being FinSequence of Y st
        1<=len f & f.1=x & f.len f in p &
        for i st 1<=i & i<len f holds
        (ex p1,p2,x0 being set st p1 in PA & p2 in PB
         & f.i in p1 & x0 in (p1 /\ p2) & f.(i+1) in p2) } as set;
    reconsider pb=union Ca as set;
    reconsider Cb={ p where p is Element of PB:
      ex q being set st q in Ca & p /\ q <> {} } as set;
    reconsider x' = x as Element of Y by A6;
    reconsider fx=<*x'*> as FinSequence of Y;
    A11:fx.1=x by FINSEQ_1:def 8;
    then A12:fx.len fx in a by A10,FINSEQ_1:57;
    A13:1<=len fx by FINSEQ_1:57;
      for i st 1<=i & i<len fx holds
        (ex p1,p2,x0 being set st p1 in PA & p2 in PB
         & fx.i in p1 & x0 in (p1 /\ p2) & fx.(i+1) in p2) by FINSEQ_1:57;
    then A14:a in Ca by A9,A10,A11,A12,A13;
    then consider y5 being set such that
      A15:x in y5 & y5 in Ca by A10;
    consider z5 being set such that
      A16:x' in z5 & z5 in PB by A4,TARSKI:def 4;
      y5 /\ z5 <> {} by A15,A16,XBOOLE_0:def 3;
    then A17:z5 in Cb by A15,A16;
    A18:pb is_a_dependent_set_of PA
    proof
        Ca c= PA
      proof
        let z be set;
        assume z in Ca;
        then ex p being Element of PA st
          z=p &
        (ex f being FinSequence of Y st
        1<=len f & f.1=x & f.len f in p &
        for i st 1<=i & i<len f holds
        (ex p1,p2,x0 being set st p1 in PA & p2 in PB
         & f.i in p1 & x0 in (p1 /\ p2) & f.(i+1) in p2));
        hence thesis;
      end;
      hence thesis by A14,Def1;
    end;
    A19:pb = union Cb
    proof
      A20:pb c= union Cb
      proof
        let x1 be set;
        assume x1 in pb;
        then consider y being set such that
          A21:x1 in y & y in Ca by TARSKI:def 4;
        consider p being Element of PA such that
          A22:y=p &
         (ex f being FinSequence of Y st
          1<=len f & f.1=x & f.len f in p &
          for i st 1<=i & i<len f holds
           (ex p1,p2,x0 being set st p1 in PA & p2 in PB
            & f.i in p1 & x0 in (p1 /\ p2) & f.(i+1) in p2)) by A21;
        consider z being set such that
          A23:x1 in z & z in PB by A4,A21,A22,TARSKI:def 4;
          y /\ z <> {} by A21,A23,XBOOLE_0:def 3;
        then x1 in z & z in Cb by A21,A23;
        hence x1 in union Cb by TARSKI:def 4;
      end;
        union Cb c= pb
      proof
        let x1 be set;
        assume x1 in union Cb;
        then consider y1 being set such that
          A24:x1 in y1 & y1 in Cb by TARSKI:def 4;
        consider p being Element of PB such that
          A25:y1=p &
         (ex q being set st q in Ca & p /\ q <> {}) by A24;
        consider q being set such that
          A26:q in Ca & y1 /\ q <> {} by A25;
        consider pd being set such that
          A27:x1 in pd & pd in PA by A3,A24,A25,TARSKI:def 4;
        consider pp being Element of PA such that
          A28:q=pp &
         (ex f being FinSequence of Y st
          1<=len f & f.1=x & f.len f in pp &
          for i st 1<=i & i<len f holds
            (ex p1,p2,x0 being set st p1 in PA & p2 in PB
            & f.i in p1 & x0 in (p1 /\ p2) & f.(i+1) in p2)) by A26;
        consider fd being FinSequence of Y such that
          A29:1<=len fd & fd.1=x & fd.len fd in q &
          for i st 1<=i & i<len fd holds
           (ex p1,p2,x0 being set st p1 in PA & p2 in PB
            & fd.i in p1 & x0 in (p1 /\ p2) & fd.(i+1) in p2) by A28;
        reconsider x1 as Element of Y by A24,A25;
        reconsider f=fd^<*x1*> as FinSequence of Y;
          len f = len fd + len <*x1*> by FINSEQ_1:35;
        then A30:len f = len fd + 1 by FINSEQ_1:57;
          1+1<=len fd + 1 by A29,AXIOMS:24;
        then A31:1<=len f by A30,AXIOMS:22;
        A32:(fd^<*x1*>).(len fd + 1)=x1 by FINSEQ_1:59;
        A33:f.(len fd + 1) in y1 by A24,FINSEQ_1:59;
          y1 meets q by A26,XBOOLE_0:def 7;
        then consider z0 being set such that
          A34:z0 in y1 & z0 in q by XBOOLE_0:3;
        A35:z0 in (y1 /\ q) by A34,XBOOLE_0:def 3;
        A36:dom fd = Seg len fd by FINSEQ_1:def 3;
        A37:for k being Nat st 1 <= k & k <= len fd holds f.k=fd.k
        proof
          let k be Nat;
          assume 1 <= k & k <= len fd;
          then k in dom fd by A36,FINSEQ_1:3;
          hence thesis by FINSEQ_1:def 7;
        end;
        then A38:f.1=x by A29;
        A39: f.len fd in q by A29,A37;
        A40:for i st 1<=i & i<len fd holds
           (ex p1,p2,x0 being set st p1 in PA & p2 in PB
            & f.i in p1 & x0 in (p1 /\ p2) & f.(i+1) in p2)
        proof
          let i;
          assume A41:1<=i & i<len fd;
          then A42:f.i = fd.i by A37;
            1<=(i+1) & (i+1)<=len fd by A41,NAT_1:38;
          then f.(i+1) = fd.(i+1) by A37;
          hence thesis by A29,A41,A42;
        end;
         for i st 1<=i & i<len f holds
           (ex p1,p2,x0 being set st p1 in PA & p2 in PB
            & f.i in p1 & x0 in (p1 /\ p2) & f.(i+1) in p2)
        proof
          let i;
          assume 1<=i & i<len f;
          then A43:1<=i & i<= len fd by A30,NAT_1:38;
            now per cases by A43,AXIOMS:21;
            case 1<=i & i<len fd;
            hence thesis by A40;
            case 1<=i & i=len fd;
            hence thesis by A25,A28,A33,A35,A39;
          end;
          hence thesis;
        end;
        then pd in Ca by A27,A30,A31,A32,A38;
        hence thesis by A27,TARSKI:def 4;
      end;
      hence thesis by A20,XBOOLE_0:def 10;
    end;
    A44:pb is_a_dependent_set_of PB
    proof
        Cb c= PB
      proof
        let z be set;
        assume z in Cb;
        then ex p being Element of PB st
          z=p &
         (ex q being set st q in Ca & p /\ q <> {});
        hence thesis;
      end;
      hence thesis by A17,A19,Def1;
    end;
      now assume not pb c= p0;
      then pb \ p0 <> {} by XBOOLE_1:37;
      then consider x1 being set such that
        A45:x1 in (pb \ p0) by XBOOLE_0:def 1;
      A46:x1 in pb & not x1 in p0 by A45,XBOOLE_0:def 4;
      then consider y1 being set such that
      A47:x1 in y1 & y1 in Cb by A19,TARSKI:def 4;
      consider p being Element of PB such that
            A48:y1=p &
           (ex q being set st q in Ca & p /\ q <> {}) by A47;
          consider q being set such that
            A49:q in Ca & y1 /\ q <> {} by A48;
          consider pp being Element of PA such that
            A50:q=pp &
           (ex f being FinSequence of Y st
            1<=len f & f.1=x & f.len f in pp &
            for i st 1<=i & i<len f holds
              (ex p1,p2,x0 being set st p1 in PA & p2 in PB
              & f.i in p1 & x0 in (p1 /\ p2) & f.(i+1) in p2)) by A49;
          consider fd being FinSequence of Y such that
            A51:1<=len fd & fd.1=x & fd.len fd in q &
            for i st 1<=i & i<len fd holds
             (ex p1,p2,x0 being set st p1 in PA & p2 in PB
              & fd.i in p1 & x0 in (p1 /\ p2) & fd.(i+1) in p2) by A50;
          reconsider x1 as Element of Y by A47,A48;
          reconsider f=fd^<*x1*> as FinSequence of Y;
           len f = len fd + len <*x1*> by FINSEQ_1:35;
          then A52:len f = len fd + 1 by FINSEQ_1:57;
            1+1<=len fd + 1 by A51,AXIOMS:24;
          then A53:1<=len f by A52,AXIOMS:22;
          A54:(fd^<*x1*>).(len fd + 1)=x1 by FINSEQ_1:59;
          A55:f.(len fd + 1) in y1 by A47,FINSEQ_1:59;
            y1 meets q by A49,XBOOLE_0:def 7;
          then consider z0 being set such that
            A56:z0 in y1 & z0 in q by XBOOLE_0:3;
          A57:z0 in (y1 /\ q) by A56,XBOOLE_0:def 3;
          A58:dom fd = Seg len fd by FINSEQ_1:def 3;
          A59:for k being Nat st 1 <= k & k <= len fd holds f.k=fd.k
          proof
            let k be Nat;
            assume 1 <= k & k <= len fd;
            then k in dom fd by A58,FINSEQ_1:3;
            hence thesis by FINSEQ_1:def 7;
          end;
          then A60:f.1=x by A51;
          A61: f.len fd in q by A51,A59;
          A62:for i st 1<=i & i<len fd holds
             (ex p1,p2,x0 being set st p1 in PA & p2 in PB
              & f.i in p1 & x0 in (p1 /\ p2) & f.(i+1) in p2)
          proof
            let i;
            assume A63:1<=i & i<len fd;
            then A64:f.i = fd.i by A59;
              1<=(i+1) & (i+1)<=len fd by A63,NAT_1:38;
            then f.(i+1) = fd.(i+1) by A59;
            hence thesis by A51,A63,A64;
          end;
          A65:for i st 1<=i & i<len f holds
             (ex p1,p2,x0 being set st p1 in PA & p2 in PB
              & f.i in p1 & x0 in (p1 /\ p2) & f.(i+1) in p2)
          proof
            let i;
            assume 1<=i & i<len f;
            then A66:1<=i & i<= len fd by A52,NAT_1:38;
              now per cases by A66,AXIOMS:21;
              case 1<=i & i<len fd;
              hence thesis by A62;
              case 1<=i & i=len fd;
              hence thesis by A48,A50,A55,A57,A61;
            end;
            hence thesis;
          end;
        for i st 1<=i & i<len f holds
             (ex p1,p2,x0 being set st p1 in PA & p2 in PB
              & f.i in p1 & x0 in p1 & x0 in p2 & f.(i+1) in p2)
      proof
        let i;
        assume 1<=i & i<len f;
        then consider p1,p2,x0 being set such that
          A67:p1 in PA & p2 in PB
              & f.i in p1 & x0 in (p1 /\ p2) & f.(i+1) in p2 by A65;
            x0 in p1 & x0 in p2 by A67,XBOOLE_0:def 3;
          hence thesis by A67;
      end;
      hence contradiction by A6,A8,A46,A52,A53,A54,A60,Th25;
    end;
    then y in pb by A6,A7,A18,A44,Def2;
        then consider y1 being set such that
          A68:y in y1 & y1 in Cb by A19,TARSKI:def 4;
        consider p being Element of PB such that
          A69:y1=p &
         (ex q being set st q in Ca & p /\ q <> {}) by A68;
        consider q being set such that
          A70:q in Ca & y1 /\ q <> {} by A69;
        consider pd being set such that
          A71:y in pd & pd in PA by A3,A68,A69,TARSKI:def 4;
        consider pp being Element of PA such that
          A72:q=pp &
         (ex f being FinSequence of Y st
          1<=len f & f.1=x & f.len f in pp &
          for i st 1<=i & i<len f holds
            (ex p1,p2,x0 being set st p1 in PA & p2 in PB
            & f.i in p1 & x0 in (p1 /\ p2) & f.(i+1) in p2)) by A70;
        consider fd being FinSequence of Y such that
          A73:1<=len fd & fd.1=x & fd.len fd in q &
          for i st 1<=i & i<len fd holds
           (ex p1,p2,x0 being set st p1 in PA & p2 in PB
            & fd.i in p1 & x0 in (p1 /\ p2) & fd.(i+1) in p2) by A72;
     reconsider y' = y as Element of Y by A6;
     reconsider f=fd^<*y'*> as FinSequence of Y;
        A74: len f = len fd + len <*y'*> by FINSEQ_1:35;
     then A75:len f = len fd + 1 by FINSEQ_1:57;
        then A76: 1+1<=len f by A73,AXIOMS:24;
        A77:(fd^<*y'*>).(len fd + 1)=y by FINSEQ_1:59;
        A78:f.(len fd + 1) in y1 by A68,FINSEQ_1:59;
          y1 meets q by A70,XBOOLE_0:def 7;
        then consider z0 being set such that
          A79:z0 in y1 & z0 in q by XBOOLE_0:3;
        A80:z0 in (y1 /\ q) by A79,XBOOLE_0:def 3;
        A81: dom fd = Seg len fd by FINSEQ_1:def 3;
        A82:for k being Nat st 1 <= k & k <= len fd holds f.k=fd.k
        proof
          let k be Nat;
          assume 1 <= k & k <= len fd;
          then k in dom fd by A81,FINSEQ_1:3;
          hence thesis by FINSEQ_1:def 7;
        end;
        then A83: f.len fd in q by A73;
        A84:for i st 1<=i & i<len fd holds
           (ex p1,p2,x0 being set st p1 in PA & p2 in PB
            & f.i in p1 & x0 in (p1 /\ p2) & f.(i+1) in p2)
        proof
          let i;
          assume A85:1<=i & i<len fd;
          then A86:f.i = fd.i by A82;
            1<=(i+1) & (i+1)<=len fd by A85,NAT_1:38;
          then f.(i+1) = fd.(i+1) by A82;
          hence thesis by A73,A85,A86;
        end;
        A87:for i st 1<=i & i<len f holds
           (ex p1,p2,x0 being set st p1 in PA & p2 in PB
            & f.i in p1 & x0 in (p1 /\ p2) & f.(i+1) in p2)
        proof
          let i;
          assume 1<=i & i<len f;
          then A88:1<=i & i<= len fd by A75,NAT_1:38;
            now per cases by A88,AXIOMS:21;
            case 1<=i & i<len fd;
            hence thesis by A84;
            case 1<=i & i=len fd;
            hence thesis by A69,A72,A78,A80,A83;
          end;
          hence thesis;
        end;
        then A89:1<=len f & f.1=x & f.len f in pd &
          for i st 1<=i & i<len f holds
           (ex p1,p2,x0 being set st p1 in PA & p2 in PB
            & f.i in p1 & x0 in (p1 /\ p2) & f.(i+1) in p2)
            by A71,A73,A74,A76,A77,A82,AXIOMS:22,FINSEQ_1:57;
      for i st 1<=i & i<len f holds
         (ex u being set st u in Y & [f.i,u] in (ERl(PA) \/ ERl(PB))
          & [u,f.(i+1)] in (ERl(PA) \/ ERl(PB)))
    proof
      let i;
      assume 1<=i & i<len f;
      then consider p1,p2,u being set such that
        A90:p1 in PA & p2 in PB &
            f.i in p1 & u in (p1 /\ p2) & f.(i+1) in p2 by A87;
      A91:p1 in PA & p2 in PB & f.i in p1 &
      u in p1 & u in p2 & f.(i+1) in p2 by A90,XBOOLE_0:def 3;
      reconsider x2=f.i as set;
      reconsider y2=f.(i+1) as set;
      A92:[x2,u] in ERl(PA) by A91,Def6;
      A93:[u,y2] in ERl(PB) by A91,Def6;
      A94:ERl(PA) c= ERl(PA) \/ ERl(PB) by XBOOLE_1:7;
        ERl(PB) c= ERl(PA) \/ ERl(PB) by XBOOLE_1:7;
      hence thesis by A91,A92,A93,A94;
    end;
     then [x',y'] in (ERl(PA) "\/" ERl(PB)) by A75,A77,A89,Th26;
    hence [x,y] in (ERl(PA) "\/" ERl(PB));
  end;
    for x1,x2 being set st [x1,x2] in (ERl(PA) \/ ERl(PB)) holds
     [x1,x2] in ERl(PA '\/' PB)
  proof
    let x1,x2 be set;
    assume [x1,x2] in (ERl(PA) \/ ERl(PB));
    then [x1,x2] in ERl(PA) or [x1,x2] in ERl(PB) by XBOOLE_0:def 2;
    then A95:(ex A being Subset of Y st A in PA & x1 in A & x2 in A) or
         (ex B being Subset of Y st B in PB & x1 in B & x2 in B) by Def6;
      now per cases by A95;
     case (x1 in Y & x2 in Y & ex A being Subset of Y
          st A in PA & x1 in A & x2 in A);
      then consider A being Subset of Y such that A96:A in PA & x1 in A & x2 in
A;
        ex y st y in (PA '\/' PB) & A c= y by A1,A96,SETFAM_1:def 2;
      hence [x1,x2] in ERl(PA '\/' PB) by A96,Def6;
     case (x1 in Y & x2 in Y & ex B being Subset of Y
          st B in PB & x1 in B & x2 in B);
      then consider B being Subset of Y such that A97:B in PB & x1 in B & x2 in
B;
        ex y st y in (PA '\/' PB) & B c= y by A2,A97,SETFAM_1:def 2;
      hence [x1,x2] in ERl(PA '\/' PB) by A97,Def6;
    end;
    hence [x1,x2] in ERl(PA '\/' PB);
  end;
  then (ERl(PA) \/ ERl(PB)) c= ERl(PA '\/' PB) by RELAT_1:def 3;
  then (ERl(PA) "\/" ERl(PB)) c= ERl(PA '\/' PB) by EQREL_1:def 3;
  hence ERl(PA '\/' PB)=(ERl(PA) "\/" ERl(PB)) by A5,XBOOLE_0:def 10;
end;

theorem Th28: for PA,PB being a_partition of Y holds
  ERl(PA '/\' PB) = ERl(PA) /\ ERl(PB)
proof let PA,PB be a_partition of Y;
  A1:PA '>' PA '/\' PB & PB '>' PA '/\' PB by Th17;
    for x1,x2 being set holds
    [x1,x2] in ERl(PA '/\' PB) iff [x1,x2] in (ERl(PA) /\ ERl(PB))
  proof
    let x1,x2 be set;
    hereby assume [x1,x2] in ERl(PA '/\' PB);
      then consider C being Subset of Y such that
        A2:C in (PA '/\' PB) & x1 in C & x2 in C by Def6;
      consider A being set such that A3:A in PA & C c= A by A1,A2,SETFAM_1:def
2;
      consider B being set such that A4:B in PB & C c= B by A1,A2,SETFAM_1:def
2;
        [x1,x2] in ERl(PA) & [x1,x2] in ERl(PB) by A2,A3,A4,Def6;
      hence [x1,x2] in (ERl(PA) /\ ERl(PB)) by XBOOLE_0:def 3;
    end;
    assume [x1,x2] in (ERl(PA) /\ ERl(PB));
then A5: [x1,x2] in ERl(PA) & [x1,x2] in ERl(PB) by XBOOLE_0:def 3;
    then consider A being Subset of Y
               such that A6:A in PA & x1 in A & x2 in A by Def6;
    consider B being Subset of Y
               such that A7:B in PB & x1 in B & x2 in B by A5,Def6;
    A8:A /\ B <> {} by A6,A7,XBOOLE_0:def 3;
    consider C being Subset of Y such that A9:C = A /\ B;
    A10:C in INTERSECTION(PA,PB) by A6,A7,A9,SETFAM_1:def 5;
      not C in {{}} by A8,A9,TARSKI:def 1;
    then C in INTERSECTION(PA,PB) \ {{}} by A10,XBOOLE_0:def 4;
    then A11:C in (PA '/\' PB) by Def4;
    A12:x1 in C by A6,A7,A9,XBOOLE_0:def 3;
      x2 in C by A6,A7,A9,XBOOLE_0:def 3;
    hence [x1,x2] in ERl(PA '/\' PB) by A11,A12,Def6;
  end;
  hence ERl(PA '/\' PB)=ERl(PA) /\ ERl(PB) by RELAT_1:def 2;
end;

theorem Th29: for PA,PB being a_partition of Y st
  ERl(PA) = ERl(PB) holds PA = PB
proof let PA,PB be a_partition of Y;
  assume ERl(PA)=ERl(PB);
  then PA '<' PB & PB '<' PA by Th24;
  hence PA=PB by Th5;
end;

theorem for PA,PB,PC being a_partition of Y holds
  (PA '\/' PB) '\/' PC = PA '\/' (PB '\/' PC)
proof
  let PA,PB,PC be a_partition of Y;
    ERl((PA '\/' PB) '\/' PC) = ERl(PA '\/' PB) "\/" ERl(PC) by Th27
                           .= (ERl(PA) "\/" ERl(PB)) "\/" ERl(PC) by Th27
                           .= ERl(PA) "\/" (ERl(PB) "\/" ERl(PC)) by MSUALG_5:1
                           .= ERl(PA) "\/" ERl(PB '\/' PC) by Th27
                           .= ERl(PA '\/' (PB '\/' PC)) by Th27;
  hence (PA '\/' PB) '\/' PC = PA '\/' (PB '\/' PC) by Th29;
end;

theorem for PA,PB being a_partition of Y holds
  PA '/\' (PA '\/' PB) = PA
proof
  let PA,PB be a_partition of Y;
  A1:ERl(PA '/\' (PA '\/' PB)) = ERl(PA) /\ ERl(PA '\/' PB) by Th28;
    ERl(PA) /\ ERl(PA '\/' PB) = ERl(PA) /\ (ERl(PA) "\/" ERl(PB)) by Th27;
  then ERl(PA '/\' (PA '\/' PB)) = ERl(PA) by A1,EQREL_1:24;
  hence PA '/\' (PA '\/' PB) = PA by Th29;
end;

theorem for PA,PB being a_partition of Y holds
  PA '\/' (PA '/\' PB) = PA
proof
  let PA,PB be a_partition of Y;
  A1:ERl(PA '\/' (PA '/\' PB)) = ERl(PA) "\/" ERl(PA '/\' PB) by Th27;
    ERl(PA) "\/" ERl(PA '/\' PB) = ERl(PA) "\/" (ERl(PA) /\ ERl(PB)) by Th28;
  then ERl(PA '\/' (PA '/\' PB)) = ERl(PA) by A1,EQREL_1:25;
  hence PA '\/' (PA '/\' PB) = PA by Th29;
end;

theorem Th33: for PA,PB,PC being a_partition of Y st
  PA '<' PC & PB '<' PC holds PA '\/' PB '<' PC
proof
  let PA,PB,PC be a_partition of Y;
  assume A1:PA '<' PC & PB '<' PC;
  then A2:ERl(PA) c= ERl(PC) by Th24;
  A3:ERl(PB) c= ERl(PC) by A1,Th24;
  A4:ERl(PA '\/' PB) = ERl(PA) "\/" ERl(PB) by Th27;
    ERl(PA) \/ ERl(PB) c= ERl(PC) by A2,A3,XBOOLE_1:8;
  then ERl(PA) "\/" ERl(PB) c= ERl(PC) by EQREL_1:def 3;
  hence thesis by A4,Th24;
end;

theorem for PA,PB,PC being a_partition of Y st
  PA '>' PC & PB '>' PC holds PA '/\' PB '>' PC
proof
  let PA,PB,PC be a_partition of Y;
  assume A1:PA '>' PC & PB '>' PC;
  then A2:ERl(PC) c= ERl(PA) by Th24;
  A3:ERl(PC) c= ERl(PB) by A1,Th24;
    ERl(PA '/\' PB) = ERl(PA) /\ ERl(PB) by Th28;
  then ERl(PC) c= ERl(PA '/\' PB) by A2,A3,XBOOLE_1:19;
  hence thesis by Th24;
end;

definition let Y;
 redefine func SmallestPartition Y;
 synonym %I(Y);
end;

definition let Y;
 canceled;

func %O(Y) -> a_partition of Y equals
 :Def9: {Y};
correctness
proof
    {Y} c= bool Y by ZFMISC_1:80;
  then A1:{Y} is Subset-Family of Y by SETFAM_1:def 7;
  A2:union {Y} = Y by ZFMISC_1:31;
    for A st A in {Y} holds A<>{} &
  for B st B in {Y} holds A = B or A misses B
  proof
    let A;
    assume A3: A in {Y};
    then A4:A=Y by TARSKI:def 1;
    thus A<>{} by A3,TARSKI:def 1;
    let B;
    assume B in {Y};
    hence thesis by A4,TARSKI:def 1;
  end;
  hence thesis by A1,A2,EQREL_1:def 6;
end;
end;

theorem %I(Y)={B:ex x being set st B={x} & x in Y}
proof
  set B0={B:ex x being set st B={x} & x in Y};
  A1:%I(Y) c= B0
  proof
    let a be set;
    assume a in %I(Y);
    then a in {{x} where x is Element of Y: not contradiction}
    by PUA2MSS1:13;
    then consider x be Element of Y such that A2:a={x};
    reconsider y=x as Element of Y;
    reconsider B={y} as Subset of Y by ZFMISC_1:37;
      a=B by A2;
    hence a in B0;
  end;
    B0 c= %I(Y)
  proof
    let x1;
    assume x1 in B0;
    then consider B such that
      A3:x1=B & (ex x being set st B={x} & x in Y);
    consider x being set such that A4:x1={x} & x in Y by A3;
      x1 in {{z} where z is Element of Y: not contradiction} by A4;
    hence x1 in %I(Y) by PUA2MSS1:13;
  end;
  hence thesis by A1,XBOOLE_0:def 10;
end;

theorem Th36:for PA being a_partition of Y holds
  %O(Y) '>' PA & PA '>' %I(Y)
proof
  let PA be a_partition of Y;
  A1: for a being set st a in PA ex b being set st b in %O(Y) & a c= b
  proof
    let a be set;
    assume a in PA;
    then A2: a c= Y & a<>{} by EQREL_1:def 6;
    consider x being Element of a;
    A3: x in Y by A2,TARSKI:def 3;
      union %O(Y) = Y by EQREL_1:def 6;
    then consider b being set such that
    A4: x in b & b in %O(Y) by A3,TARSKI:def 4;
      %O(Y) = {Y} by Def9;
    then a c= b by A2,A4,TARSKI:def 1;
    hence thesis by A4;
  end;
    for a being set st a in %I(Y) ex b being set st b in PA & a c= b
  proof
    let a be set;
    assume A5:a in %I(Y);
    then a in {{x} where x is Element of Y: not contradiction}
    by PUA2MSS1:13;
    then consider x be Element of Y such that A6:a={x};
    A7: a c= Y & a<>{} by A5,EQREL_1:def 6;
    consider u being Element of a;
    A8:u=x by A6,TARSKI:def 1;
    A9: u in Y by A7,TARSKI:def 3;
      union PA = Y by EQREL_1:def 6;
    then consider b being set such that A10: u in b & b in PA by A9,TARSKI:def
4;
      a c= b
    proof
      let x1;
      assume x1 in a;
      hence thesis by A6,A8,A10,TARSKI:def 1;
    end;
    hence thesis by A10;
  end;
  hence thesis by A1,SETFAM_1:def 2;
end;

theorem Th37: ERl(%O(Y)) = nabla Y
proof
  A1:ERl(%O(Y)) c= nabla Y
  proof
    let x1,x2 be set;
    assume [x1,x2] in ERl(%O(Y));
    then [x1,x2] in [:Y,Y:];
    hence [x1,x2] in nabla Y by EQREL_1:def 1;
  end;
    nabla Y c= ERl(%O(Y))
  proof
    let x1,x2 be set;
    assume A2: [x1,x2] in nabla Y;
      Y in {Y} by TARSKI:def 1;
    then Y in %O(Y) & x1 in Y & x2 in Y by A2,Def9,ZFMISC_1:106;
    hence [x1,x2] in ERl(%O(Y)) by Def6;
  end;
  hence thesis by A1,XBOOLE_0:def 10;
end;

theorem Th38: ERl(%I(Y)) = id Y
proof
  A1:union %I(Y)=Y by EQREL_1:def 6;
  A2:ERl(%I(Y)) c= id Y
  proof
    let x1,x2 be set;
    assume [x1,x2] in ERl(%I(Y));
    then consider a being Subset of Y such that
      A3:a in %I(Y) & x1 in a & x2 in a by Def6;
      %I(Y) = {{x} where x is Element of Y: not contradiction}
                   by PUA2MSS1:13;
    then consider x be Element of Y such that A4:a={x} by A3;
    A5:x1=x by A3,A4,TARSKI:def 1;
      x2=x by A3,A4,TARSKI:def 1;
    hence [x1,x2] in id Y by A5,RELAT_1:def 10;
  end;
    id Y c= ERl(%I(Y))
  proof
    let x1,x2 be set;
    assume [x1,x2] in id Y;
    then A6: x1 in Y & x1=x2 by RELAT_1:def 10;
    then ex y being set st x1 in y & y in %I(Y) by A1,TARSKI:def 4;
    hence [x1,x2] in ERl(%I(Y)) by A6,Def6;
  end;
  hence thesis by A2,XBOOLE_0:def 10;
end;

theorem %I(Y) '<' %O(Y)
proof
    ERl(%O(Y)) = nabla Y by Th37
               .= [:Y,Y:] by EQREL_1:def 1;
  then ERl(%I(Y)) c= ERl(%O(Y));
  hence thesis by Th24;
end;

theorem for PA being a_partition of Y holds
  %O(Y) '\/' PA = %O(Y) & %O(Y) '/\' PA = PA
proof
  let PA be a_partition of Y;
  thus %O(Y) '\/' PA = %O(Y)
  proof
    A1:ERl(%O(Y) '\/' PA) = ERl(%O(Y)) "\/" ERl(PA) by Th27;
      ERl(%O(Y)) = nabla Y by Th37;
    then ERl(%O(Y)) \/ ERl(PA) = ERl(%O(Y)) by MSUALG_5:4;
    then ERl(%O(Y)) c= ERl(%O(Y)) "\/" ERl(PA) by EQREL_1:def 3;
    then A2:%O(Y) '<' %O(Y) '\/' PA by A1,Th24;
     %O(Y) '>' PA '\/' %O(Y) by Th36;
    hence thesis by A2,Th5;
  end;
  thus %O(Y) '/\' PA = PA
  proof
    A3:ERl(%O(Y) '/\' PA) = ERl(%O(Y)) /\ ERl(PA) by Th28;
      ERl(%O(Y)) = nabla Y by Th37;
    then ERl(%O(Y) '/\' PA) = ERl(PA) by A3,EQREL_1:18;
    hence %O(Y) '/\' PA = PA by Th29;
  end;
end;

theorem for PA being a_partition of Y holds
  %I(Y) '\/' PA = PA & %I(Y) '/\' PA = %I(Y)
proof
  let PA be a_partition of Y;
  thus %I(Y) '\/' PA = PA
  proof
    A1:ERl(%I(Y) '\/' PA) = ERl(%I(Y)) "\/" ERl(PA) by Th27;
    A2:ERl(%I(Y)) = id Y by Th38;
    A3:ERl(%I(Y)) \/ ERl(PA) c= ERl(%I(Y)) "\/" ERl(PA)
      by EQREL_1:def 3;
    A4:ERl(%I(Y)) \/ ERl(PA) = id Y \/ ERl(PA) by Th38;
      %I(Y) '<' PA by Th36;
    then A5:ERl(%I(Y)) c= ERl(PA) by Th24;
      id Y \/ ERl(PA) = ERl(PA)
    proof
       for z being set st z in id Y \/ ERl(PA) holds z in ERl PA
      proof
        let z be set;
        assume A6: z in id Y \/ ERl(PA);
          now per cases by A6,XBOOLE_0:def 2;
         case z in id Y;
          hence thesis by A2,A5;
         case z in ERl(PA);
          hence thesis;
        end;
        hence thesis;
      end;
      then A7:id Y \/ ERl(PA) c= ERl(PA) by TARSKI:def 3;
        ERl(PA) c= id Y \/ ERl(PA) by XBOOLE_1:7;
      hence thesis by A7,XBOOLE_0:def 10;
    end;
    then A8:PA '<' %I(Y) '\/' PA by A1,A3,A4,Th24;
      %I(Y) '<' PA by Th36;
    then %I(Y) '\/' PA '<' PA by Th33;
    hence %I(Y) '\/' PA = PA by A8,Th5;
  end;
  thus %I(Y) '/\' PA = %I(Y)
  proof
      ERl(%I(Y) '/\' PA) = ERl(%I(Y)) /\ ERl(PA) by Th28
                      .= id Y /\ ERl(PA) by Th38
                      .= id Y by EQREL_1:17
                      .= ERl(%I(Y)) by Th38;
    hence thesis by Th29;
  end;
end;

Back to top