:: Equivalence Relations and Classes of Abstraction
::  by Konrad Raczkowski and Pawe{\l} Sadowski
::
:: Received November 16, 1989
:: Copyright (c) 1990-2012 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 NUMBERS, SUBSET_1, RELAT_1, ZFMISC_1, SETFAM_1, TARSKI, PARTFUN1,
      RELAT_2, XBOOLE_0, FINSEQ_1, XXREAL_0, FUNCT_1, ARYTM_3, ORDINAL4,
      ARYTM_1, NAT_1, CARD_1, EQREL_1, MCART_1, CARD_3;
 notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, MCART_1, DOMAIN_1, SUBSET_1,
      XCMPLX_0, XXREAL_0, RELAT_1, RELAT_2, SETFAM_1, FINSEQ_1, FUNCT_1,
      NUMBERS, ORDINAL1, NAT_1, FUNCT_3, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1;
 constructors SETFAM_1, RELAT_2, PARTFUN1, XXREAL_0, XREAL_0, NAT_1, FINSEQ_1,
      RELSET_1, FUNCT_3, BINOP_1, DOMAIN_1, XTUPLE_0;
 registrations XBOOLE_0, SUBSET_1, PARTFUN1, XXREAL_0, XREAL_0, FINSEQ_1,
      RELAT_1, ORDINAL1, RELSET_1, FUNCT_2, FUNCT_3, ZFMISC_1, FUNCT_1,
      RELAT_2, XTUPLE_0;
 requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
 definitions TARSKI, RELAT_1, RELAT_2, XBOOLE_0, PARTFUN1, SETFAM_1, SUBSET_1,
      BINOP_1, XTUPLE_0;
 theorems RELAT_1, RELAT_2, RELSET_1, SETFAM_1, ZFMISC_1, TARSKI, FINSEQ_1,
      NAT_1, XBOOLE_0, XBOOLE_1, ORDERS_1, PARTFUN1, XREAL_1, XXREAL_0,
      FUNCT_1, FUNCT_3, FUNCT_2, MCART_1, SUBSET_1, SETWISEO, XTUPLE_0;
 schemes SUBSET_1, RELSET_1, FINSEQ_1, NAT_1, FUNCT_2;

begin

reserve X,Y,Z,x,y,z for set;
reserve i,j for Element of NAT;
reserve A,B,C for Subset of X;
reserve R,R1,R2 for Relation of X;
reserve AX for Subset of [:X,X:];
reserve SFXX for Subset-Family of [:X,X:];

:: Equivalence Relation and its properties

definition
  let X;
  func nabla X -> Relation of X equals
  [:X,X:];
  coherence
  proof
    [:X,X:] c=[:X,X:];
    hence thesis;
  end;
end;

registration
  let X;
  cluster nabla X -> total reflexive;
  coherence
  proof
    thus dom nabla X c= X;
    thus X c= dom nabla X
    proof
      let x be set;
      assume x in X;
      then [x,x] in [:X,X:] by ZFMISC_1:87;
      hence thesis by XTUPLE_0:def 12;
    end;
    let x;
    assume x in field nabla X;
    then x in dom nabla X \/ rng nabla X;
    hence thesis by ZFMISC_1:87;
  end;
end;

definition
  let X;
  let R1,R2;
  redefine func R1 /\ R2 -> Relation of X;
  coherence
  proof
    R1 /\ R2 c= [:X,X:];
    hence thesis;
  end;
  redefine func R1 \/ R2 -> Relation of X;
  coherence
  proof
    R1 \/ R2 c= [:X,X:];
    hence thesis;
  end;
end;

theorem
  nabla X \/ R1 = nabla X by XBOOLE_1:12;

theorem
  id X is_reflexive_in X & id X is_symmetric_in X & id X is_transitive_in X
proof
  thus for x st x in X holds [x,x] in id X by RELAT_1:def 10;
  thus for x,y st x in X & y in X & [x,y] in id X holds [y,x] in id X by
RELAT_1:def 10;
  thus for x,y,z st x in X & y in X & z in X & [x,y] in id X & [y,z] in id X
  holds [x,z] in id X by RELAT_1:def 10;
end;

definition
  let X;
  mode Tolerance of X is total reflexive symmetric Relation of X;
  mode Equivalence_Relation of X is total symmetric transitive Relation of X;
end;

theorem
  id X is Equivalence_Relation of X;

theorem Th4:
  nabla X is Equivalence_Relation of X
proof
  for x,y holds x in X & y in X & [x,y] in nabla X implies [y,x] in nabla
  X by ZFMISC_1:88;
  then
A1: nabla X is_symmetric_in X by RELAT_2:def 3;
  for x,y,z st x in X & y in X & z in X & [x,y] in nabla X & [y,z] in
  nabla X holds [x,z] in nabla X by ZFMISC_1:87;
  then
A2: nabla X is_transitive_in X by RELAT_2:def 8;
  field nabla X = X by ORDERS_1:12;
  hence thesis by A1,A2,RELAT_2:def 11,def 16;
end;

registration
  let X;
  cluster nabla X -> total symmetric transitive;
  coherence by Th4;
end;

reserve EqR,EqR1,EqR2,EqR3 for Equivalence_Relation of X;

Lm1: [x,y] in R implies x in X & y in X
proof
  assume [x,y] in R;
  then x in dom R & y in rng R by XTUPLE_0:def 12,def 13;
  hence thesis;
end;

theorem Th5:
  for R being total reflexive Relation of X holds x in X implies [ x,x] in R
proof
  let R be total reflexive Relation of X;
  field R = X by ORDERS_1:12;
  then R is_reflexive_in X by RELAT_2:def 9;
  hence thesis by RELAT_2:def 1;
end;

theorem Th6:
  for R being total symmetric Relation of X holds [x,y] in R implies [y,x] in R
proof
  let R be total symmetric Relation of X;
  field R = X by ORDERS_1:12;
  then
A1: R is_symmetric_in X by RELAT_2:def 11;
  assume
A2: [x,y] in R;
  then x in X & y in X by Lm1;
  hence thesis by A2,A1,RELAT_2:def 3;
end;

theorem Th7:
  for R being total transitive Relation of X holds [x,y] in R & [y
  ,z] in R implies [x,z] in R
proof
  let R be total transitive Relation of X;
  assume that
A1: [x,y] in R and
A2: [y,z] in R;
A3: z in X by A2,Lm1;
  field R = X by ORDERS_1:12;
  then
A4: R is_transitive_in X by RELAT_2:def 16;
  x in X & y in X by A1,Lm1;
  hence thesis by A1,A2,A3,A4,RELAT_2:def 8;
end;

theorem
  for R being total reflexive Relation of X holds (ex x being set st x
  in X) implies R <> {};

theorem Th9:
  R is Equivalence_Relation of X iff R is reflexive symmetric
  transitive & field R = X
proof
  thus R is Equivalence_Relation of X implies R is reflexive symmetric
  transitive & field R = X by ORDERS_1:12;
  assume that
A1: R is reflexive and
A2: R is symmetric & R is transitive and
A3: field R = X;
  R is_reflexive_in X by A1,A3,RELAT_2:def 9;
  then dom R = X by ORDERS_1:13;
  hence thesis by A2,PARTFUN1:def 2;
end;

definition
  let X;
  let EqR1,EqR2;
  redefine func EqR1 /\ EqR2 -> Equivalence_Relation of X;
  coherence
  proof
    for x st x in X holds [x,x] in EqR2 by Th5;
    then
A1: id X c= EqR2 by RELAT_1:47;
    for x st x in X holds [x,x] in EqR1 by Th5;
    then id X c= EqR1 by RELAT_1:47;
    then id X c= EqR1 /\ EqR2 by A1,XBOOLE_1:19;
    then dom(EqR1 /\ EqR2) = X & rng(EqR1 /\ EqR2) = X by RELSET_1:16,17;
    then field (EqR1 /\ EqR2) = X;
    hence thesis by Th9;
  end;
end;

theorem
  id X /\ EqR = id X
proof
  now
    let x,y;
    assume [x,y] in id X;
    then x in X & x = y by RELAT_1:def 10;
    hence [x,y] in EqR by Th5;
  end;
  then id X c= EqR by RELAT_1:def 3;
  hence thesis by XBOOLE_1:28;
end;

theorem Th11:
  for SFXX st (SFXX <> {} & for Y st Y in SFXX holds Y is
  Equivalence_Relation of X) holds meet SFXX is Equivalence_Relation of X
proof
  let SFXX such that
A1: SFXX <> {} and
A2: for Y st Y in SFXX holds Y is Equivalence_Relation of X;
  reconsider XX = meet SFXX as Relation of X;
A3: XX is_symmetric_in X
  proof
    let x,y;
    assume that
    x in X and
    y in X and
A4: [x,y] in XX;
    now
      let Y;
      assume Y in SFXX;
      then Y is Equivalence_Relation of X & [x,y] in Y by A2,A4,SETFAM_1:def 1;
      hence [y,x] in Y by Th6;
    end;
    hence thesis by A1,SETFAM_1:def 1;
  end;
A5: XX is_transitive_in X
  proof
    let x,y,z;
    assume that
    x in X and
    y in X and
    z in X and
A6: [x,y] in XX and
A7: [y,z] in XX;
    now
      let Y;
      assume
A8:   Y in SFXX;
      then
A9:   [y,z] in Y by A7,SETFAM_1:def 1;
      Y is Equivalence_Relation of X & [x,y] in Y by A2,A6,A8,SETFAM_1:def 1;
      hence [x,z] in Y by A9,Th7;
    end;
    hence thesis by A1,SETFAM_1:def 1;
  end;
  XX is_reflexive_in X
  proof
    let x such that
A10: x in X;
    for Y st Y in SFXX holds [x,x] in Y
    proof
      let Y;
      assume Y in SFXX;
      then Y is Equivalence_Relation of X by A2;
      hence thesis by A10,Th5;
    end;
    hence thesis by A1,SETFAM_1:def 1;
  end;
  then field XX = X & dom XX = X by ORDERS_1:13;
  hence thesis by A3,A5,PARTFUN1:def 2,RELAT_2:def 11,def 16;
end;

theorem Th12:
  for R holds ex EqR st R c= EqR & for EqR2 st R c= EqR2 holds EqR c= EqR2
proof
  let R;
  defpred P[set] means $1 is Equivalence_Relation of X & R c= $1;
  consider F being Subset-Family of [:X,X:] such that
A1: for AX holds AX in F iff P[AX] from SUBSET_1:sch 3;
  R c= nabla X;
  then
A2: F <> {} by A1;
  for Y st Y in F holds Y is Equivalence_Relation of X by A1;
  then reconsider EqR = meet F as Equivalence_Relation of X by A2,Th11;
A3: now
    let EqR2;
    assume R c= EqR2;
    then EqR2 in F by A1;
    hence EqR c= EqR2 by SETFAM_1:3;
  end;
  take EqR;
  for Y st Y in F holds R c= Y by A1;
  hence thesis by A2,A3,SETFAM_1:5;
end;

definition
  let X;
  let EqR1,EqR2;

  func EqR1 "\/" EqR2 -> Equivalence_Relation of X means
  :Def2:
  EqR1 \/ EqR2 c= it & for EqR st EqR1 \/ EqR2 c= EqR holds it c= EqR;
  existence by Th12;
  uniqueness
  proof
    let R1,R2 be Equivalence_Relation of X;
    assume EqR1 \/ EqR2 c= R1 & ( for EqR st EqR1 \/ EqR2 c= EqR holds R1 c=
    EqR)& EqR1 \/ EqR2 c= R2 & for EqR st EqR1 \/ EqR2 c= EqR holds R2 c= EqR;
    then R1 c= R2 & R2 c= R1;
    hence thesis by XBOOLE_0:def 10;
  end;
  commutativity;
  idempotence;
end;

theorem
  (EqR1 "\/" EqR2) "\/" EqR3 = EqR1 "\/" (EqR2 "\/" EqR3)
proof
  for EqR4 be Equivalence_Relation of X holds EqR4 = EqR1 "\/" (EqR2 "\/"
  EqR3) implies (EqR1 "\/" EqR2) "\/" EqR3 c= EqR4
  proof
    let EqR4 be Equivalence_Relation of X;
A1: EqR2 \/ EqR3 c= EqR2 "\/" EqR3 by Def2;
    assume EqR4 = EqR1 "\/" (EqR2 "\/" EqR3);
    then
A2: EqR1 \/ (EqR2 "\/" EqR3) c= EqR4 by Def2;
    EqR2 "\/" EqR3 c= EqR1 \/ (EqR2 "\/" EqR3) by XBOOLE_1:7;
    then EqR2 "\/" EqR3 c= EqR4 by A2,XBOOLE_1:1;
    then
A3: EqR2 \/ EqR3 c= EqR4 by A1,XBOOLE_1:1;
    EqR2 c= EqR2 \/ EqR3 by XBOOLE_1:7;
    then
A4: EqR2 c= EqR4 by A3,XBOOLE_1:1;
    EqR1 c= EqR1 \/ (EqR2 "\/" EqR3) by XBOOLE_1:7;
    then EqR1 c= EqR4 by A2,XBOOLE_1:1;
    then EqR1 \/ EqR2 c= EqR4 by A4,XBOOLE_1:8;
    then
A5: EqR1 "\/" EqR2 c= EqR4 by Def2;
    EqR3 c= EqR2 \/ EqR3 by XBOOLE_1:7;
    then EqR3 c= EqR4 by A3,XBOOLE_1:1;
    then (EqR1 "\/" EqR2) \/ EqR3 c= EqR4 by A5,XBOOLE_1:8;
    hence thesis by Def2;
  end;
  then
A6: (EqR1 "\/" EqR2) "\/" EqR3 c= EqR1 "\/" (EqR2 "\/" EqR3);
  for EqR4 be Equivalence_Relation of X holds EqR4 = (EqR1 "\/" EqR2) "\/"
  EqR3 implies EqR1 "\/" (EqR2 "\/" EqR3) c= EqR4
  proof
    let EqR4 be Equivalence_Relation of X;
A7: EqR1 \/ EqR2 c= EqR1 "\/" EqR2 by Def2;
    assume EqR4 = (EqR1 "\/" EqR2) "\/" EqR3;
    then
A8: (EqR1 "\/" EqR2) \/ EqR3 c= EqR4 by Def2;
    EqR1 "\/" EqR2 c= (EqR1 "\/" EqR2) \/ EqR3 by XBOOLE_1:7;
    then EqR1 "\/" EqR2 c= EqR4 by A8,XBOOLE_1:1;
    then
A9: EqR1 \/ EqR2 c= EqR4 by A7,XBOOLE_1:1;
    EqR3 c= (EqR1 "\/" EqR2) \/ EqR3 by XBOOLE_1:7;
    then
A10: EqR3 c= EqR4 by A8,XBOOLE_1:1;
    EqR2 c= EqR1 \/ EqR2 by XBOOLE_1:7;
    then EqR2 c= EqR4 by A9,XBOOLE_1:1;
    then EqR2 \/ EqR3 c= EqR4 by A10,XBOOLE_1:8;
    then
A11: EqR2 "\/" EqR3 c= EqR4 by Def2;
    EqR1 c= EqR1 \/ EqR2 by XBOOLE_1:7;
    then EqR1 c= EqR4 by A9,XBOOLE_1:1;
    then EqR1 \/ (EqR2 "\/" EqR3) c= EqR4 by A11,XBOOLE_1:8;
    hence thesis by Def2;
  end;
  then EqR1 "\/" (EqR2 "\/" EqR3) c= (EqR1 "\/" EqR2) "\/" EqR3;
  hence thesis by A6,XBOOLE_0:def 10;
end;

theorem
  EqR "\/" EqR = EqR;

theorem
  EqR1 "\/" EqR2 = EqR2 "\/" EqR1;

theorem
  EqR1 /\ (EqR1 "\/" EqR2) = EqR1
proof
  thus EqR1 /\ (EqR1 "\/" EqR2) c= EqR1 by XBOOLE_1:17;
  EqR1 c= EqR1 \/ EqR2 & EqR1 \/ EqR2 c= EqR1 "\/" EqR2 by Def2,XBOOLE_1:7;
  then EqR1 c= EqR1 "\/" EqR2 by XBOOLE_1:1;
  hence thesis by XBOOLE_1:19;
end;

theorem
  EqR1 "\/" (EqR1 /\ EqR2) = EqR1
proof
  EqR1 = EqR1 \/ (EqR1 /\ EqR2) & for EqR st EqR1 \/ (EqR1 /\ EqR2) c= EqR
  holds EqR1 c= EqR by XBOOLE_1:22;
  hence thesis by Def2;
end;

scheme
  ExEqRel {X() -> set,P[set,set]}: ex EqR being Equivalence_Relation of X() st
  for x,y holds [x,y] in EqR iff x in X() & y in X() & P[x,y]
provided
A1: for x st x in X() holds P[x,x] and
A2: for x,y st P[x,y] holds P[y,x] and
A3: for x,y,z st P[x,y] & P[y,z] holds P[x,z]
proof
  consider Y being Relation of X(),X() such that
A4: for x,y holds [x,y] in Y iff x in X() & y in X() & P[x,y] from
  RELSET_1:sch 1;
A5: Y is_transitive_in X()
  proof
    let x,y,z;
    assume that
A6: x in X() and
    y in X() and
A7: z in X() and
A8: [x,y] in Y & [y,z] in Y;
    ( P[x,y])& P[y,z] by A4,A8;
    then P[x,z] by A3;
    hence thesis by A4,A6,A7;
  end;
A9: Y is_symmetric_in X()
  proof
    let x,y;
    assume that
A10: x in X() & y in X() and
A11: [x,y] in Y;
    P[x,y] by A4,A11;
    then P[y,x] by A2;
    hence thesis by A4,A10;
  end;
  Y is_reflexive_in X()
  proof
    let x;
    assume
A12: x in X();
    then P[x,x] by A1;
    hence thesis by A4,A12;
  end;
  then field Y = X() & dom Y = X() by ORDERS_1:13;
  then reconsider R1 = Y as Equivalence_Relation of X() by A9,A5,PARTFUN1:def 2
,RELAT_2:def 11,def 16;
  take R1;
  thus thesis by A4;
end;

:: Classes of abstraction

notation
  let R be Relation, x be set;
  synonym Class(R,x) for Im(R,x);
end;

definition
  let X, Y be set, R be Relation of X, Y, x be set;

  redefine func Class(R,x) -> Subset of Y;
  coherence
  proof
    R.:{x} c= Y;
    hence thesis;
  end;
end;

theorem
  for R being Relation holds y in Class (R,x) iff [x,y] in R
proof
  let R be Relation;
  thus y in Class(R,x) implies [x,y] in R
  proof
    assume y in Class(R,x);
    then ex z being set st [z,y] in R & z in {x} by RELAT_1:def 13;
    hence thesis by TARSKI:def 1;
  end;
A1: x in {x} by TARSKI:def 1;
  assume [x,y] in R;
  hence thesis by A1,RELAT_1:def 13;
end;

theorem Th19:
  for R being total symmetric Relation of X holds y in Class (R,x)
  iff [y,x] in R
proof
  let R be total symmetric Relation of X;
  thus y in Class(R,x) implies [y,x] in R
  proof
    assume y in Class(R,x);
    then ex z being set st [z,y] in R & z in {x} by RELAT_1:def 13;
    then [x,y] in R by TARSKI:def 1;
    hence thesis by Th6;
  end;
  assume [y,x] in R;
  then
A1: [x,y] in R by Th6;
  x in {x} by TARSKI:def 1;
  hence thesis by A1,RELAT_1:def 13;
end;

theorem Th20:
  for R being Tolerance of X holds for x st x in X holds x in Class (R,x)
proof
  let R be Tolerance of X;
  let x;
  assume x in X;
  then [x,x] in R by Th5;
  hence thesis by Th19;
end;

theorem
  for R being Tolerance of X holds for x st x in X holds ex y st x in
  Class(R,y)
proof
  let R be Tolerance of X;
  let x;
  assume x in X;
  then x in Class(R,x) by Th20;
  hence thesis;
end;

theorem
  for R being transitive Tolerance of X holds y in Class(R,x) & z in
  Class(R,x) implies [y,z] in R
proof
  let R be transitive Tolerance of X;
  assume that
A1: y in Class(R,x) and
A2: z in Class(R,x);
  [z,x] in R by A2,Th19;
  then
A3: [x,z] in R by Th6;
  [y,x] in R by A1,Th19;
  hence thesis by A3,Th7;
end;

Lm2: for x st x in X holds [x,y] in EqR iff Class(EqR,x) = Class(EqR,y)
proof
  let x such that
A1: x in X;
  thus [x,y] in EqR implies Class(EqR,x) = Class(EqR,y)
  proof
    assume
A2: [x,y] in EqR;
    now
      let z;
      assume z in Class(EqR,y);
      then
A3:   [z,y] in EqR by Th19;
      [y,x] in EqR by A2,Th6;
      then [z,x] in EqR by A3,Th7;
      hence z in Class(EqR,x) by Th19;
    end;
    then
A4: Class(EqR,y) c= Class(EqR,x) by TARSKI:def 3;
    now
      let z;
      assume z in Class(EqR,x);
      then [z,x] in EqR by Th19;
      then [z,y] in EqR by A2,Th7;
      hence z in Class(EqR,y) by Th19;
    end;
    then Class(EqR,x) c= Class(EqR,y) by TARSKI:def 3;
    hence thesis by A4,XBOOLE_0:def 10;
  end;
  assume Class(EqR,x) = Class(EqR,y);
  then x in Class(EqR,y) by A1,Th20;
  hence thesis by Th19;
end;

theorem Th23:
  for x st x in X holds y in Class(EqR,x) iff Class(EqR,x) = Class (EqR,y)
proof
  let x such that
A1: x in X;
  thus y in Class(EqR,x) implies Class(EqR,x) = Class(EqR,y)
  proof
    assume y in Class(EqR,x);
    then [y,x] in EqR by Th19;
    then [x,y] in EqR by Th6;
    hence thesis by A1,Lm2;
  end;
  assume Class(EqR,x) = Class(EqR,y);
  then [x,y] in EqR by A1,Lm2;
  then [y,x] in EqR by Th6;
  hence thesis by Th19;
end;

theorem Th24:
  for x,y st y in X holds Class(EqR,x) = Class(EqR,y) or Class(EqR
  ,x) misses Class(EqR,y)
proof
  let x,y;
A1: not [x,y] in EqR implies Class(EqR,x) misses Class(EqR,y)
  proof
    assume
A2: not [x,y] in EqR;
    assume Class(EqR,x) meets Class(EqR,y);
    then consider z such that
A3: z in Class(EqR,x) and
A4: z in Class(EqR,y) by XBOOLE_0:3;
    [z,x] in EqR by A3,Th19;
    then
A5: [x,z] in EqR by Th6;
    [z,y] in EqR by A4,Th19;
    hence contradiction by A2,A5,Th7;
  end;
  assume
A6: y in X;
  [x,y] in EqR implies Class(EqR,x) = Class(EqR,y)
  proof
    assume [x,y] in EqR;
    then x in Class(EqR,y) by Th19;
    hence thesis by A6,Th23;
  end;
  hence thesis by A1;
end;

theorem Th25:
  for x st x in X holds Class(id X,x) = {x}
proof
  let x;
A1: now
    let y;
    assume y in Class(id X,x);
    then [y,x] in id X by Th19;
    hence y = x by RELAT_1:def 10;
  end;
  assume x in X;
  then for y holds y in Class(id X,x) iff y = x by A1,Th20;
  hence thesis by TARSKI:def 1;
end;

theorem Th26:
  for x st x in X holds Class(nabla X,x) = X
proof
  let x such that
A1: x in X;
  now
    let y;
    assume y in X;
    then [y,x] in nabla X by A1,ZFMISC_1:87;
    hence y in Class(nabla X,x) by Th19;
  end;
  then for y holds y in X iff y in Class(nabla X,x);
  hence thesis by TARSKI:1;
end;

theorem Th27:
  (ex x st Class(EqR,x) = X) implies EqR = nabla X
proof
  given x such that
A1: Class(EqR,x) = X;
  [:X,X:] c= EqR
  proof
    let y,z;
    assume
A2: [y,z] in [:X,X:];
    then z in Class(EqR,x) by A1,ZFMISC_1:87;
    then [z,x] in EqR by Th19;
    then
A3: [x,z] in EqR by Th6;
    y in Class(EqR,x) by A1,A2,ZFMISC_1:87;
    then [y,x] in EqR by Th19;
    hence thesis by A3,Th7;
  end;
  hence thesis by XBOOLE_0:def 10;
end;

theorem
  x in X implies ([x,y] in EqR1 "\/" EqR2 iff ex f being FinSequence st
1 <= len f & x = f.1 & y = f.(len f) & for i st 1 <= i & i < len f holds [f.i,f
  .(i+1)] in EqR1 \/ EqR2)
proof
  assume
A1: x in X;
  thus [x,y] in EqR1 "\/" EqR2 implies ex f being FinSequence st 1 <= len f &
  x = f.1 & y = f.(len f) & for i st 1 <= i & i < len f holds [f.i,f.(i+1)] in
  EqR1 \/ EqR2
  proof
    defpred P[set,set] means ex f being FinSequence st (1 <= len f & $1 = f.1
& $2 = f.(len f) & for i st 1 <= i & i < len f holds [f.i,f.(i+1)] in EqR1 \/
    EqR2);
    consider Y being Relation of X,X such that
A2: for x,y holds [x,y] in Y iff x in X & y in X & P[x,y] from
    RELSET_1:sch 1;
A3: Y is_transitive_in X
    proof
      let x,y,z;
      assume that
A4:   x in X and
A5:   y in X and
A6:   z in X and
A7:   [x,y] in Y and
A8:   [y,z] in Y;
      consider g being FinSequence such that
A9:   1 <= len g and
A10:  y = g.1 and
A11:  z = g.(len g) and
A12:  for i st 1 <= i & i < len g holds [g.i,g.(i+1)] in EqR1 \/ EqR2 by A2,A8;
      consider f being FinSequence such that
A13:  1 <= len f and
A14:  x = f.1 and
A15:  y = f.(len f) and
A16:  for i st 1 <= i & i < len f holds [f.i,f.(i+1)] in EqR1 \/ EqR2 by A2,A7;
      set h = f^g;
A17:  len h = len f + len g by FINSEQ_1:22;
A18:  len f + 1 <= len f + len g by A9,XREAL_1:7;
      then
A19:  h.(len h) = g.(len g + len f - len f) by A17,FINSEQ_1:23
        .= g.(len g);
A20:  for i st 1 <= i & i < len h holds [h.i,h.(i+1)] in EqR1 \/ EqR2
      proof
        let i;
        assume that
A21:    1 <= i and
A22:    i < len h;
A23:    1 <= i & i < len f or i = len f or len f < i by A21,XXREAL_0:1;
        now
          per cases by A22,A23,NAT_1:13;
          suppose
A24:        1 <= i & i < len f;
            then 1 <= i + 1 & i + 1 <= len f by NAT_1:13;
            then i + 1 in Seg len f by FINSEQ_1:1;
            then i + 1 in dom f by FINSEQ_1:def 3;
            then
A25:        h.(i + 1) = f.(i + 1) by FINSEQ_1:def 7;
            i in Seg(len f) by A24,FINSEQ_1:1;
            then i in dom f by FINSEQ_1:def 3;
            then h.i = f.i by FINSEQ_1:def 7;
            hence thesis by A16,A24,A25;
          end;
          suppose
A26:        i = len f;
            len f in Seg len f by A13,FINSEQ_1:1;
            then len f in dom f by FINSEQ_1:def 3;
            then
A27:        h.i = y by A15,A26,FINSEQ_1:def 7;
A28:        [y,y] in EqR1 by A5,Th5;
            h.(i + 1) = g.(1 + len f - len f) by A18,A26,FINSEQ_1:23
              .= y by A10;
            hence thesis by A27,A28,XBOOLE_0:def 3;
          end;
          suppose
A29:        len f + 1 <= i & i < len h;
            then len f < i by NAT_1:13;
            then reconsider k = i - len f as Element of NAT by NAT_1:21;
            i < len f + len g by A29,FINSEQ_1:22;
            then
A30:        i - len f < len g by XREAL_1:19;
            len f + 1 <= i + 1 & i + 1 <= len f + len g by A17,A29,NAT_1:13;
            then
A31:        h.(i + 1) = g.(1 + i - len f) by FINSEQ_1:23
              .= g.((i - len f) + 1);
            1 + len f - len f <= i - len f by A29,XREAL_1:9;
            then [g.k,g.(k + 1)] in EqR1 \/ EqR2 by A12,A30;
            hence thesis by A17,A29,A31,FINSEQ_1:23;
          end;
        end;
        hence thesis;
      end;
      1 in Seg(len f) by A13,FINSEQ_1:1;
      then 1 in dom f by FINSEQ_1:def 3;
      then
A32:  x = h.1 by A14,FINSEQ_1:def 7;
      1 <= len h by A13,A17,NAT_1:12;
      hence thesis by A2,A4,A6,A11,A32,A19,A20;
    end;
A33: Y is_symmetric_in X
    proof
      let x,y;
      assume that
A34:  x in X & y in X and
A35:  [x,y] in Y;
      consider f being FinSequence such that
A36:  1 <= len f and
A37:  x = f.1 and
A38:  y = f.(len f) and
A39:  for i st 1 <= i & i < len f holds [f.i,f.(i+1)] in EqR1 \/ EqR2
      by A2,A35;
      defpred P[Nat,set] means $2 = f.(1 + (len f) - $1);
A40:  for k be Nat st k in Seg(len f) ex z st P[k,z];
      consider g being FinSequence such that
A41:  dom g = Seg(len f) & for k being Nat st k in Seg(len f) holds P
      [k,g.k] from FINSEQ_1:sch 1(A40);
A42:  len f = len g by A41,FINSEQ_1:def 3;
A43:  for j st 1 <= j & j < len g holds [g.j,g.(j+1)] in EqR1 \/ EqR2
      proof
        let j;
        assume that
A44:    1 <= j and
A45:    j < len g;
        reconsider k = (len f) - j as Element of NAT by A42,A45,NAT_1:21;
        j - (len f) < (len f) - (len f) by A42,A45,XREAL_1:9;
        then - ((len f) - j) < - 0;
        then 0 < k;
        then
A46:    0 + 1 <= k by NAT_1:13;
        - j < -0 by A44,XREAL_1:24;
        then (len f) + -j < 0 + (len f) by XREAL_1:6;
        then
A47:    [f.k,f.(k + 1)] in EqR1 \/ EqR2 by A39,A46;
A48:    now
          per cases by A47,XBOOLE_0:def 3;
          suppose
            [f.k,f.(k + 1)] in EqR1;
            then [f.(k + 1),f.k] in EqR1 by Th6;
            hence [f.(k + 1),f.k] in EqR1 \/ EqR2 by XBOOLE_0:def 3;
          end;
          suppose
            [f.k,f.(k + 1)] in EqR2;
            then [f.(k + 1),f.k] in EqR2 by Th6;
            hence [f.(k + 1),f.k] in EqR1 \/ EqR2 by XBOOLE_0:def 3;
          end;
        end;
        1 <= (j + 1) & (j + 1) <= len f by A42,A45,NAT_1:12,13;
        then (j + 1) in Seg(len f) by FINSEQ_1:1;
        then
A49:    g.(j + 1) = f.((len f) + 1 - (1 + j)) by A41
          .= f.((len f) - j);
        j in Seg(len f) by A42,A44,A45,FINSEQ_1:1;
        then g.j = f.(1 + (len f) - j) by A41
          .= f.(((len f) - j) + 1);
        hence thesis by A49,A48;
      end;
      len f in Seg(len f) by A36,FINSEQ_1:1;
      then g.(len f) = f.(1 + (len f) - len f) by A41
        .= f.(1 + 0);
      then
A50:  x = g.(len g) by A37,A41,FINSEQ_1:def 3;
      1 in Seg(len f) by A36,FINSEQ_1:1;
      then
A51:  g.1 = f.((len f) + 1 - 1) by A41
        .= f.(len f);
      1 <= len g by A36,A41,FINSEQ_1:def 3;
      hence thesis by A2,A34,A38,A51,A50,A43;
    end;
    Y is_reflexive_in X
    proof
      let x such that
A52:  x in X;
      set g = <*x*>;
A53:  for i st 1 <= i & i < len g holds [g.i,g.(i+1)] in EqR1 \/ EqR2 by
FINSEQ_1:40;
      len g = 1 & g.1 = x by FINSEQ_1:40;
      hence thesis by A2,A52,A53;
    end;
    then field Y = X & dom Y = X by ORDERS_1:13;
    then reconsider R1 = Y as Equivalence_Relation of X by A33,A3,
PARTFUN1:def 2,RELAT_2:def 11,def 16;
    for x,y holds [x,y] in EqR1 \/ EqR2 implies [x,y] in R1
    proof
      let x,y;
      assume
A54:  [x,y] in EqR1 \/ EqR2;
      set g = <*x,y*>;
A55:  len g = 1 + 1 by FINSEQ_1:44;
A56:  g.1 = x by FINSEQ_1:44;
A57:  for i st 1 <= i & i < len g holds [g.i,g.(i+1)] in EqR1 \/ EqR2
      proof
        let i;
        assume that
A58:    1 <= i and
A59:    i < len g;
        i <= 1 by A55,A59,NAT_1:13;
        then 1 = i by A58,XXREAL_0:1;
        hence thesis by A54,A56,FINSEQ_1:44;
      end;
      len g = 2 by FINSEQ_1:44;
      then
A60:  g.1 = x & g.(len g) = y by FINSEQ_1:44;
      x in X & y in X by A54,Lm1;
      hence thesis by A2,A55,A60,A57;
    end;
    then EqR1 \/ EqR2 c= R1 by RELAT_1:def 3;
    then
A61: EqR1 "\/" EqR2 c= R1 by Def2;
    assume [x,y] in EqR1 "\/" EqR2;
    then consider f being FinSequence such that
A62: 1 <= len f & x = f.1 &( y = f.(len f) & for i st 1 <= i & i <
    len f holds [f.i,f.(i+1)] in EqR1 \/ EqR2 ) by A2,A61;
    take f;
    thus thesis by A62;
  end;
  given f being FinSequence such that
A63: 1 <= len f and
A64: x = f.1 and
A65: y = f.(len f) and
A66: for i st 1 <= i & i < len f holds [f.i,f.(i+1)] in EqR1 \/ EqR2;
  defpred P[Element of NAT] means 1 <= $1 & $1 <= len f implies [f.1,f.$1] in
  EqR1 "\/" EqR2;
A67: now
    let i;
    assume
A68: P[i];
    thus P[i+1]
    proof
      assume that
A69:  1 <= i + 1 and
A70:  i + 1 <= len f;
A71:  1 <= i or 1 = i + 1 by A69,NAT_1:8;
A72:  EqR1 \/ EqR2 c= EqR1 "\/" EqR2 by Def2;
A73:  i < len f by A70,NAT_1:13;
      now
        per cases by A71;
        suppose
A74:      1 <= i;
          then [f.i,f.(i+1)] in EqR1 \/ EqR2 by A66,A73;
          hence thesis by A68,A70,A72,A74,Th7,NAT_1:13;
        end;
        suppose
A75:      0 = i;
          [f.1,f.1] in EqR1 by A1,A64,Th5;
          then [f.1,f.1] in EqR1 \/ EqR2 by XBOOLE_0:def 3;
          hence thesis by A72,A75;
        end;
      end;
      hence thesis;
    end;
  end;
A76: P[0];
  for i holds P[i] from NAT_1:sch 1(A76,A67);
  hence thesis by A63,A64,A65;
end;

theorem Th29:
  for E being Equivalence_Relation of X st E = EqR1 \/ EqR2 holds
for x st x in X holds Class(E,x) = Class(EqR1,x) or Class(E,x) = Class(EqR2,x)
proof
  let E be Equivalence_Relation of X such that
A1: E = EqR1 \/ EqR2;
  for x st x in X holds Class(E,x) = Class(EqR1,x) or Class(E,x) = Class(
  EqR2,x)
  proof
    let x such that
    x in X;
    assume that
A2: not Class(E,x) = Class(EqR1,x) and
A3: not Class(E,x) = Class(EqR2,x);
    consider y such that
A4: y in Class(E,x) & not y in Class(EqR1,x) or y in Class(EqR1,x) &
    not y in Class(E,x) by A2,TARSKI:1;
A5: now
      assume that
A6:   y in Class(EqR1,x) and
A7:   not y in Class(E,x);
      [y,x] in EqR1 by A6,Th19;
      then [y,x] in E by A1,XBOOLE_0:def 3;
      hence contradiction by A7,Th19;
    end;
    then
A8: [y,x] in E by A4,Th19;
    consider z such that
A9: z in Class(E,x) & not z in Class(EqR2,x) or z in Class(EqR2,x) &
    not z in Class(E,x) by A3,TARSKI:1;
A10: now
      assume that
A11:  z in Class(EqR2,x) and
A12:  not z in Class(E,x);
      [z,x] in EqR2 by A11,Th19;
      then [z,x] in E by A1,XBOOLE_0:def 3;
      hence contradiction by A12,Th19;
    end;
    then
A13: [z,x] in E by A9,Th19;
    not [z,x] in EqR2 by A9,A10,Th19;
    then
A14: [z,x] in EqR1 by A1,A13,XBOOLE_0:def 3;
A15: now
      assume [y,z] in EqR1;
      then
A16:  [z,y] in EqR1 by Th6;
      [x,z] in EqR1 by A14,Th6;
      then [x,y] in EqR1 by A16,Th7;
      then [y,x] in EqR1 by Th6;
      hence contradiction by A4,A5,Th19;
    end;
    not [y,x] in EqR1 by A4,A5,Th19;
    then
A17: [y,x] in EqR2 by A1,A8,XBOOLE_0:def 3;
A18: now
      assume
A19:  [y,z] in EqR2;
      [x,y] in EqR2 by A17,Th6;
      then [x,z] in EqR2 by A19,Th7;
      then [z,x] in EqR2 by Th6;
      hence contradiction by A9,A10,Th19;
    end;
    [x,z] in E by A13,Th6;
    then [y,z] in E by A8,Th7;
    hence contradiction by A1,A18,A15,XBOOLE_0:def 3;
  end;
  hence thesis;
end;

theorem
  EqR1 \/ EqR2 = nabla X implies EqR1 = nabla X or EqR2 = nabla X
proof
  assume
A1: EqR1 \/ EqR2 = nabla X;
  (not X = {}) implies EqR1 = nabla X or EqR2 = nabla X
  proof
    set y = the Element of X;
A2: now
      let x;
      assume
A3:   x in X;
      then
      Class(nabla X,x) = Class(EqR1,x) or Class(nabla X,x) = Class(EqR2,x)
      by A1,Th29;
      hence Class(EqR1,x) = X or Class(EqR2,x) = X by A3,Th26;
    end;
    assume X <> {};
    then Class(EqR1,y) = X or Class(EqR2,y) = X by A2;
    hence thesis by Th27;
  end;
  hence thesis;
end;

definition
  let X;
  let EqR;
  func Class EqR -> Subset-Family of X means
  :Def3:
  A in it iff ex x st x in X & A = Class(EqR,x);
  existence
  proof
    defpred P[set] means ex x st x in X & $1 = Class(EqR,x);
    consider F being Subset-Family of X such that
A1: for A holds A in F iff P[A] from SUBSET_1:sch 3;
    take F;
    thus thesis by A1;
  end;
  uniqueness
  proof
    let F1,F2 be Subset-Family of X;
    assume that
A2: for A holds A in F1 iff ex x st x in X & A = Class(EqR,x) and
A3: for A holds A in F2 iff ex x st x in X & A = Class(EqR,x);
    now
      let A;
      A in F1 iff ex x st x in X & A = Class(EqR,x) by A2;
      hence A in F1 iff A in F2 by A3;
    end;
    hence thesis by SETFAM_1:31;
  end;
end;

theorem Th31:
  X = {} implies Class EqR = {}
proof
  assume that
A1: X = {} and
A2: Class EqR <> {};
  set z = the Element of Class EqR;
  z is Subset of X by A2,TARSKI:def 3;
  then ex x st x in X & z = Class(EqR,x) by A2,Def3;
  hence contradiction by A1;
end;

definition
  let X;
  mode a_partition of X -> Subset-Family of X means
    :Def4:
    union it = X & for
    A st A in it holds A<>{} & for B st B in it holds A = B or A misses B;
  existence
  proof
    defpred P[set] means ex x st x in X & $1 = {x};
    consider F being Subset-Family of X such that
A1: for A being Subset of X holds A in F iff P[A] from SUBSET_1:sch 3;
A2: for A st A in F holds A<>{} & for B st B in F holds A = B or A misses B
    proof
      let A;
      assume A in F;
      then consider x such that
      x in X and
A3:   A = {x} by A1;
      thus A <> {} by A3;
      let B;
      assume B in F;
      then consider y such that
      y in X and
A4:   B = {y} by A1;
      now
        assume
A5:     not x = y;
        for z st z in A holds not z in B
        proof
          let z;
          assume z in A;
          then not z = y by A3,A5,TARSKI:def 1;
          hence thesis by A4,TARSKI:def 1;
        end;
        hence A misses B by XBOOLE_0:3;
      end;
      hence thesis by A3,A4;
    end;
    take F;
    now
      let y;
      now
        set Z = {y};
        assume
A6:     y in X;
        then Z is Subset of X by ZFMISC_1:31;
        then y in Z & Z in F by A1,A6,TARSKI:def 1;
        hence ex Z st y in Z & Z in F;
      end;
      hence y in X iff ex Z st y in Z & Z in F;
    end;
    hence thesis by A2,TARSKI:def 4;
  end;
end;

theorem Th32:
  for P being a_partition of {} holds P = {}
proof
  let P be a_partition of {};
  assume not thesis;
  then consider Z being set such that
A1: Z in P by XBOOLE_0:def 1;
  Z <> {} by A1,Def4;
  hence thesis by A1;
end;

theorem Th33:
  Class EqR is a_partition of X
proof
  now
    let x;
    now
      consider Z such that
A1:   Z = Class(EqR,x);
      assume
A2:   x in X;
      then Z in Class EqR by A1,Def3;
      hence ex Z st x in Z & Z in Class EqR by A2,A1,Th20;
    end;
    hence x in X iff ex Z st x in Z & Z in Class EqR;
  end;
  hence union(Class EqR) = X by TARSKI:def 4;
  let A;
  assume A in Class EqR;
  then
A3: ex x st x in X & A = Class(EqR,x) by Def3;
  hence A <> {} by Th20;
  let B;
  assume B in Class EqR;
  then ex y st y in X & B = Class(EqR,y) by Def3;
  hence thesis by A3,Th24;
end;

theorem Th34:
  for P being a_partition of X holds ex EqR st P = Class EqR
proof
  let P be a_partition of X;
A1: X <> {} implies ex EqR st P = Class EqR
  proof
    defpred P[set,set] means ex A st A in P & $1 in A & $2 in A;
    assume X <> {};
A2: for x,y,z st P[x,y] & P[y,z] holds P[x,z]
    proof
      let x,y,z;
      given A such that
A3:   A in P and
A4:   x in A & y in A;
      given B such that
A5:   B in P and
A6:   y in B & z in B;
      A = B or A misses B by A3,A5,Def4;
      hence thesis by A3,A4,A6,XBOOLE_0:3;
    end;
A7: union P = X by Def4;
A8: for x st x in X holds P[x,x]
    proof
      let x;
      assume x in X;
      then consider Z such that
A9:   x in Z and
A10:  Z in P by A7,TARSKI:def 4;
      reconsider A = Z as Subset of X by A10;
      take A;
      thus thesis by A9,A10;
    end;
A11: for x,y st P[x,y] holds P[y,x];
    consider R being Equivalence_Relation of X such that
A12: for x,y holds [x,y] in R iff x in X & y in X & P[x,y] from
    ExEqRel(A8,A11,A2);
    take R;
    now
      let A;
A13:  now
        set x = the Element of A;
        assume
A14:    A in P;
        then
A15:    A <> {} by Def4;
        then
A16:    x in X by TARSKI:def 3;
        now
          let y;
A17:      now
            assume y in Class(R,x);
            then [y,x] in R by Th19;
            then consider B such that
A18:        B in P & y in B and
A19:        x in B by A12;
            A meets B by A15,A19,XBOOLE_0:3;
            hence y in A by A14,A18,Def4;
          end;
          now
            assume y in A;
            then [y,x] in R by A12,A14,A16;
            hence y in Class(R,x) by Th19;
          end;
          hence y in A iff y in Class(R,x) by A17;
        end;
        then A = Class(R,x) by TARSKI:1;
        hence A in Class R by A16,Def3;
      end;
      now
        assume A in Class R;
        then consider x such that
A20:    x in X and
A21:    A = Class(R,x) by Def3;
        x in Class(R,x) by A20,Th20;
        then [x,x] in R by Th19;
        then consider B such that
A22:    B in P and
A23:    x in B and
        x in B by A12;
        now
          let y;
A24:      now
            assume y in A;
            then [y,x] in R by A21,Th19;
            then consider C such that
A25:        C in P & y in C and
A26:        x in C by A12;
            B meets C by A23,A26,XBOOLE_0:3;
            hence y in B by A22,A25,Def4;
          end;
          now
            assume y in B;
            then [y,x] in R by A12,A22,A23;
            hence y in A by A21,Th19;
          end;
          hence y in A iff y in B by A24;
        end;
        hence A in P by A22,TARSKI:1;
      end;
      hence A in P iff A in Class R by A13;
    end;
    hence thesis by SETFAM_1:31;
  end;
  X = {} implies ex EqR st P = Class EqR
  proof
    set EqR1 = the Equivalence_Relation of X;
    assume
A27: X = {};
    take EqR1;
    P = {} by A27,Th32;
    hence thesis by A27,Th31;
  end;
  hence thesis by A1;
end;

theorem
  for x st x in X holds [x,y] in EqR iff Class(EqR,x) = Class(EqR,y) by Lm2;

theorem
  x in Class EqR implies ex y being Element of X st x = Class(EqR,y)
proof
  assume
A1: x in Class EqR;
  then reconsider x as Subset of X;
  consider y such that
A2: y in X and
A3: x = Class(EqR,y) by A1,Def3;
  reconsider y as Element of X by A2;
  take y;
  thus thesis by A3;
end;

begin :: Addenda
:: from FSM_1, PARTIT1, 2005.02.06, A.T.

registration
  let X be non empty set;
  cluster -> non empty for a_partition of X;
  coherence
  proof
    set x = the Element of X;
    let P be a_partition of X;
    union P = X by Def4;
    then ex A being set st x in A & A in P by TARSKI:def 4;
    hence thesis;
  end;
end;

:: from PUA2MSS1

registration
  let X be set;
  cluster -> with_non-empty_elements for a_partition of X;
  coherence
  proof
    let P be a_partition of X;
    assume {} in P;
    hence contradiction by Def4;
  end;
end;

definition
  let X be set, R be Equivalence_Relation of X;
  redefine func Class R -> a_partition of X;
  coherence by Th33;
end;

:: from PRALG_3

registration
  let I be non empty set, R be Equivalence_Relation of I;
  cluster Class R -> non empty;
  coherence;
end;

registration
  let I be non empty set, R be Equivalence_Relation of I;
  cluster Class R -> with_non-empty_elements;
  coherence;
end;

notation
  let I be non empty set, R be Equivalence_Relation of I;
  let x be Element of I;
  synonym EqClass(R,x) for Class(R,x);
end;

definition
  let I be non empty set, R be Equivalence_Relation of I;
  let x be Element of I;
  redefine func EqClass(R,x) -> Element of Class R;
  coherence
  proof
    thus Class(R,x) is Element of Class R by Def3;
  end;
end;

definition
  let X be set;
  func SmallestPartition X -> a_partition of X equals
  Class id X;
  coherence;
end;

theorem
  for X being non empty set holds SmallestPartition X = {{x} where x is
  Element of X: not contradiction}
proof
  let X be non empty set;
  set Y = {{x} where x is Element of X: not contradiction};
  hereby
    let x be set;
    assume x in SmallestPartition X;
    then consider y being set such that
A1: y in X and
A2: x = Class(id X, y) by Def3;
    x = {y} by A1,A2,Th25;
    hence x in Y by A1;
  end;
  let x be set;
  assume x in Y;
  then consider y being Element of X such that
A3: x = {y};
  Class(id X, y) = x by A3,Th25;
  hence thesis by Def3;
end;

:: from T_1TOPSP, 30.12.2006, AK
:: Classes of partitions of a set

reserve X for non empty set,
  x for Element of X;

definition
  let X be non empty set,x be Element of X,S1 be a_partition of X;
  func EqClass(x,S1) -> Subset of X means
  :Def6:
  x in it & it in S1;
  existence
  proof
    consider EQR being Equivalence_Relation of X such that
A1: S1 = Class EQR by Th34;
    take Class(EQR,x);
    thus x in Class(EQR,x) by Th20;
    thus thesis by A1,Def3;
  end;
  uniqueness
  proof
    let A,B be Subset of X;
    assume that
A2: x in A and
A3: A in S1 and
A4: x in B and
A5: B in S1;
    A meets B by A2,A4,XBOOLE_0:3;
    hence thesis by A3,A5,Def4;
  end;
end;

theorem Th38:
  for S1,S2 being a_partition of X st (for x being Element of X
  holds EqClass(x,S1) = EqClass(x,S2)) holds S1=S2
proof
  let S1,S2 be a_partition of X;
  assume
A1: for x being Element of X holds EqClass(x,S1) = EqClass(x,S2);
  now
    let P be Subset of X;
    thus P in S1 implies P in S2
    proof
      set x = the Element of P;
      assume
A2:   P in S1;
      then
A3:   P is non empty by Def4;
      then x in P;
      then reconsider x as Element of X;
      P = EqClass(x,S1) by A2,A3,Def6;
      then P = EqClass(x,S2) by A1;
      hence thesis by Def6;
    end;
    thus P in S2 implies P in S1
    proof
      set x = the Element of P;
      assume
A4:   P in S2;
      then
A5:   P <> {} by Def4;
      then x in P;
      then reconsider x as Element of X;
      P = EqClass(x,S2) by A4,A5,Def6;
      then P = EqClass(x,S1) by A1;
      hence thesis by Def6;
    end;
  end;
  hence thesis by SETFAM_1:31;
end;

theorem Th39:
  for X being non empty set holds {X} is a_partition of X
proof
  let X be non empty set;
  reconsider A1 = {X} as Subset-Family of X by ZFMISC_1:68;
A1: for A being Subset of X st A in A1 holds A <> {} & for B being Subset of
  X st B in A1 holds A = B or A misses B
  proof
    let A be Subset of X;
    assume
A2: A in A1;
    hence A <> {} by TARSKI:def 1;
    let B be Subset of X;
    assume B in A1;
    then B = X by TARSKI:def 1;
    hence thesis by A2,TARSKI:def 1;
  end;
  union A1 = X by ZFMISC_1:25;
  hence thesis by A1,Def4;
end;

definition
  let X be set;
  mode Family-Class of X is Subset-Family of bool X;
end;

definition

  let X be set;
  let F be Family-Class of X;
  attr F is partition-membered means
  :Def7:
  for S being set st S in F holds S is a_partition of X;
end;

registration
  let X be set;
  cluster partition-membered for Family-Class of X;
  existence
  proof
    reconsider E = {} as Family-Class of X by XBOOLE_1:2;
    take E;
    let S be set;
    assume S in E;
    hence thesis;
  end;
end;

definition
  let X be set;
  mode Part-Family of X is partition-membered Family-Class of X;
end;

reserve F for Part-Family of X;

registration
  let X be non empty set;
  cluster non empty for a_partition of X;
  existence
  proof
    take {X};
    thus thesis by Th39;
  end;
end;

theorem Th40:
  for X being set, p being a_partition of X holds {p} is Part-Family of X
proof
  let X be set;
  let p be a_partition of X;
  for x be set st x in {p} holds x is a_partition of X by TARSKI:def 1;
  hence thesis by Def7;
end;

registration
  let X be set;
  cluster non empty for Part-Family of X;
  existence
  proof
    set p = the a_partition of X;
    reconsider P = {p} as Part-Family of X by Th40;
    take P;
    thus thesis;
  end;
end;

theorem Th41:
  for S1 being a_partition of X, x,y being Element of X holds
  EqClass(x,S1) meets EqClass(y,S1) implies EqClass(x,S1) = EqClass(y,S1)
proof
  let S1 be a_partition of X;
  let x,y be Element of X;
  consider EQR being Equivalence_Relation of X such that
A1: S1 = Class EQR by Th34;
A2: y in Class(EQR,y) by Th20;
  Class(EQR,y) in S1 by A1,Def3;
  then
A3: Class(EQR,y) = EqClass(y,S1) by A2,Def6;
A4: x in Class(EQR,x) by Th20;
  Class(EQR,x) in S1 by A1,Def3;
  then
A5: Class(EQR,x) = EqClass(x,S1) by A4,Def6;
  assume EqClass(x,S1) meets EqClass(y,S1);
  hence thesis by A5,A3,Th24;
end;

Lm3: for A being set holds A in {EqClass(x,S) where S is a_partition of X : S
in F} implies ex T being a_partition of X st T in F & A = EqClass(x,T)
proof
  let A be set;
  assume A in {EqClass(x,S) where S is a_partition of X : S in F};
  then consider S being a_partition of X such that
A1: A = EqClass(x,S) & S in F;
  take S;
  thus thesis by A1;
end;

theorem
  for A being set,X being non empty set,S being a_partition of X holds A
  in S implies ex x being Element of X st A = EqClass(x,S)
proof
  let A be set,X be non empty set,S be a_partition of X;
  assume
A1: A in S;
  then A is non empty by Def4;
  then consider x being set such that
A2: x in A by XBOOLE_0:def 1;
  take x;
  thus thesis by A1,A2,Def6;
end;

definition
  let X be non empty set,F be non empty Part-Family of X;
  func Intersection F -> non empty a_partition of X means
  for x being Element
of X holds EqClass(x,it) = meet{EqClass(x,S) where S is a_partition of X : S in
  F};
  uniqueness
  proof
    given S1,S2 being a_partition of X such that
A1: for x being Element of X holds EqClass(x,S1) = meet{EqClass(x,S)
    where S is a_partition of X : S in F} and
A2: for x being Element of X holds EqClass(x,S2) = meet{EqClass(x,S)
    where S is a_partition of X : S in F} and
A3: not S1 = S2;
    now
      let x be Element of X;
      EqClass(x,S1) = meet{EqClass(x,S) where S is a_partition of X : S in
      F} by A1;
      hence EqClass(x,S1) = EqClass(x,S2) by A2;
    end;
    hence contradiction by A3,Th38;
  end;
  existence
  proof
    thus ex G being non empty a_partition of X st for x being Element of X
holds EqClass(x,G) = meet{EqClass(x,S) where S is a_partition of X : S in F}
    proof
      set G = {meet{EqClass(x,S) where S is a_partition of X : S in F} where x
      is Element of X : not contradiction };
      G c= bool X
      proof
        let y be set;
        assume y in G;
        then consider x being Element of X such that
A4:     y = meet{EqClass(x,S) where S is a_partition of X : S in F};
        y c= X
        proof
          let e be set;
          consider T being set such that
A5:       T in F by XBOOLE_0:def 1;
          reconsider T as a_partition of X by A5,Def7;
          EqClass(x,T) in {EqClass(x,S) where S is a_partition of X : S
          in F } by A5;
          then consider f being set such that
A6:       f in {EqClass(x,S) where S is a_partition of X : S in F};
          consider S being a_partition of X such that
A7:       f = EqClass(x,S) and
          S in F by A6;
          assume e in y;
          then e in EqClass(x,S) by A4,A6,A7,SETFAM_1:def 1;
          hence thesis;
        end;
        hence thesis;
      end;
      then reconsider G as Subset-Family of X;
      G is a_partition of X
      proof
        X c= union G
        proof
          let a be set;
          consider T being set such that
A8:       T in F by XBOOLE_0:def 1;
          assume a in X;
          then reconsider a1=a as Element of X;
          reconsider T as a_partition of X by A8,Def7;
A9:       meet{EqClass(a1,S) where S is a_partition of X : S in F} in G;
A10:      for T being set st T in {EqClass(a1,S) where S is a_partition
          of X : S in F} holds a1 in T
          proof
            let T be set;
            assume T in {EqClass(a1,S) where S is a_partition of X : S in F};
            then ex A being a_partition of X st T = EqClass(a1,A) & A in F;
            hence thesis by Def6;
          end;
          EqClass(a1,T) in {EqClass(a1,S) where S is a_partition of X : S
          in F} by A8;
          then
          a in meet{EqClass(a1,S) where S is a_partition of X: S in F} by A10,
SETFAM_1:def 1;
          hence thesis by A9,TARSKI:def 4;
        end;
        hence union G = X by XBOOLE_0:def 10;
        let A be Subset of X;
        consider T being set such that
A11:    T in F by XBOOLE_0:def 1;
        reconsider T as a_partition of X by A11,Def7;
        assume
A12:    A in G;
        then consider x being Element of X such that
A13:    A = meet{EqClass(x,S) where S is a_partition of X : S in F};
A14:    for Y being set st Y in {EqClass(x,S) where S is a_partition of X
        : S in F} holds x in Y
        proof
          let Y be set;
          assume Y in {EqClass(x,S) where S is a_partition of X : S in F};
          then ex T being a_partition of X st Y = EqClass(x,T) & T in F;
          hence thesis by Def6;
        end;
        EqClass(x,T) in {EqClass(x,S) where S is a_partition of X : S in
        F} by A11;
        hence A<>{} by A13,A14,SETFAM_1:def 1;
        consider x being Element of X such that
A15:    A = meet{EqClass(x,S) where S is a_partition of X : S in F} by A12;
        let B be Subset of X;
        assume B in G;
        then consider y being Element of X such that
A16:    B = meet{EqClass(y,S) where S is a_partition of X : S in F};
        thus A = B or A misses B
        proof
A17:      {EqClass(y,S) where S is a_partition of X : S in F} is non empty
          proof
            consider T being set such that
A18:        T in F by XBOOLE_0:def 1;
            reconsider T as a_partition of X by A18,Def7;
            EqClass(y,T) in {EqClass(y,S) where S is a_partition of X : S
            in F} by A18;
            hence thesis;
          end;
A19:      {EqClass(x,S) where S is a_partition of X : S in F} is non empty
          proof
            consider T being set such that
A20:        T in F by XBOOLE_0:def 1;
            reconsider T as a_partition of X by A20,Def7;
            EqClass(x,T) in {EqClass(x,S) where S is a_partition of X : S
            in F} by A20;
            hence thesis;
          end;
          now
            assume A meets B;
            then consider c being set such that
A21:        c in A & c in B by XBOOLE_0:3;
            c in meet{EqClass(x,S) where S is a_partition of X : S in F}
/\ meet{EqClass(y,S) where S is a_partition of X : S in F} by A15,A16,A21,
XBOOLE_0:def 4;
            then
A22:        c in meet({EqClass(x,S) where S is a_partition of X: S in F }
\/ {EqClass(y,S) where S is a_partition of X : S in F}) by A19,A17,SETFAM_1:9;
A23:        now
              let T be a_partition of X;
              assume T in F;
              then
              EqClass(y,T) in {EqClass(y,S) where S is a_partition of X :
              S in F};
              then
              EqClass(y,T) in {EqClass(x,S) where S is a_partition of X :
S in F} \/ {EqClass(y,S) where S is a_partition of X : S in F} by
XBOOLE_0:def 3;
              hence c in EqClass(y,T) by A22,SETFAM_1:def 1;
            end;
A24:        now
              let T be a_partition of X;
              assume T in F;
              then
              EqClass(x,T) in {EqClass(x,S) where S is a_partition of X :
              S in F};
              then
              EqClass(x,T) in {EqClass(x,S) where S is a_partition of X :
S in F} \/ {EqClass(y,S) where S is a_partition of X : S in F} by
XBOOLE_0:def 3;
              hence c in EqClass(x,T) by A22,SETFAM_1:def 1;
            end;
A25:        for T being a_partition of X st T in F holds ex A being set
            st A in EqClass(x,T) & A in EqClass(y,T)
            proof
              let T be a_partition of X;
              assume
A26:          T in F;
              take c;
              thus thesis by A24,A23,A26;
            end;
A27:        for T being a_partition of X st T in F holds (EqClass(x,T))
            meets (EqClass(y,T))
            proof
              let T be a_partition of X;
              assume T in F;
              then ex A being set st A in EqClass(x,T) & A in EqClass(y,T) by
A25;
              hence thesis by XBOOLE_0:3;
            end;
A28:        {EqClass(y,S) where S is a_partition of X : S in F} c= {
            EqClass(x,S) where S is a_partition of X : S in F}
            proof
              let A be set;
              assume A in {EqClass(y,S) where S is a_partition of X : S in F };
              then consider T being a_partition of X such that
A29:          T in F and
A30:          A = EqClass(y,T) by Lm3;
              A = EqClass(x,T) by A27,A29,A30,Th41;
              hence thesis by A29;
            end;
            {EqClass(x,S) where S is a_partition of X : S in F} c= {
            EqClass(y,S) where S is a_partition of X : S in F}
            proof
              let A be set;
              assume A in {EqClass(x,S) where S is a_partition of X : S in F };
              then consider T being a_partition of X such that
A31:          T in F and
A32:          A = EqClass(x,T) by Lm3;
              A = EqClass(y,T) by A27,A31,A32,Th41;
              hence thesis by A31;
            end;
            hence thesis by A15,A16,A28,XBOOLE_0:def 10;
          end;
          hence thesis;
        end;
      end;
      then reconsider G as non empty a_partition of X;
      take G;
      for x being Element of X holds EqClass(x,G) = meet{EqClass(x,S)
      where S is a_partition of X : S in F}
      proof
        let x be Element of X;
A33:    now
          let Y be set;
          assume Y in {EqClass(x,S) where S is a_partition of X : S in F};
          then ex T being a_partition of X st Y = EqClass(x,T) & T in F;
          hence x in Y by Def6;
        end;
        {EqClass(x,S) where S is a_partition of X : S in F} is non empty
        proof
          consider T being set such that
A34:      T in F by XBOOLE_0:def 1;
          reconsider T as a_partition of X by A34,Def7;
          EqClass(x,T) in {EqClass(x,S) where S is a_partition of X : S
          in F} by A34;
          hence thesis;
        end;
        then meet{EqClass(x,S) where S is a_partition of X : S in F} in G & x
in meet{ EqClass(x,S) where S is a_partition of X : S in F} by A33,
SETFAM_1:def 1;
        hence thesis by Def6;
      end;
      hence thesis;
    end;
  end;
end;

theorem Th43:
  for X being non empty set, S being a_partition of X, A being
  Subset of S holds (union S) \ (union A) = union (S \ A)
proof
  let X be non empty set;
  let S be a_partition of X;
  let A be Subset of S;
  thus (union S) \ (union A) c= union (S \ A)
  proof
    let y be set;
    assume
A1: y in (union S) \ (union A);
    then y in (union S) by XBOOLE_0:def 5;
    then consider z being set such that
A2: y in z and
A3: z in S by TARSKI:def 4;
    not y in (union A) by A1,XBOOLE_0:def 5;
    then not z in A by A2,TARSKI:def 4;
    then z in S \ A by A3,XBOOLE_0:def 5;
    hence thesis by A2,TARSKI:def 4;
  end;
  thus union (S \ A) c= (union S) \ (union A)
  proof
    let y be set;
    assume y in union(S \ A);
    then consider z being set such that
A4: y in z and
A5: z in S \ A by TARSKI:def 4;
A6: z in S by A5,XBOOLE_0:def 5;
A7: not z in A by A5,XBOOLE_0:def 5;
A8: now
      let w be set;
      assume
A9:   w in A;
      then w in S;
      then z misses w by A6,A7,A9,Def4;
      hence not y in w by A4,XBOOLE_0:3;
    end;
A10: now
      assume y in union A;
      then ex v being set st y in v & v in A by TARSKI:def 4;
      hence contradiction by A8;
    end;
    y in union S by A4,A6,TARSKI:def 4;
    hence thesis by A10,XBOOLE_0:def 5;
  end;
end;

theorem
  for X being non empty set,A being Subset of X, S being a_partition of
  X holds A in S implies union(S \ {A}) = X \ A
proof
  let X be non empty set;
  let A be Subset of X;
  let S be a_partition of X;
  assume
A1: A in S;
  {A} c= S
  proof
    let y be set;
    assume y in {A};
    hence thesis by A1,TARSKI:def 1;
  end;
  then reconsider AA = {A} as Subset of S;
  thus union (S \ {A}) = (union S) \ (union AA) by Th43
    .= X \ (union {A}) by Def4
    .= X \ A by ZFMISC_1:25;
end;

:: Added 2007.10.17, AK

theorem
  {} is a_partition of {}
proof
  reconsider A = {} as Subset-Family of {} by XBOOLE_1:2;
  union A = {} & for a be Subset of {} st a in A holds a<>{} & for b be
  Subset of {} st b in A holds a = b or a misses b;
  hence thesis by Def4;
end;

begin :: Moved from BORSUK_1, 2010.03.15, A.T.

reserve e,u,v,X,Y,X1 for set;

theorem
  for F being Function st X c= F"X1 holds F.:X c= X1
proof
  let F be Function;
  assume X c= F"X1;
  then
A1: F.:X c= F.:F"X1 by RELAT_1:123;
  F.:F"X1 c= X1 by FUNCT_1:75;
  hence thesis by A1,XBOOLE_1:1;
end;

theorem Th47:
  e c= [:X,Y:] implies (.:pr1(X,Y)).e = pr1(X,Y).:e
proof
  assume e c= [:X,Y:];
  then e c= dom pr1(X,Y) by FUNCT_3:def 4;
  hence thesis by FUNCT_3:def 1;
end;

theorem Th48:
  e c= [:X,Y:] implies (.:pr2(X,Y)).e = pr2(X,Y).:e
proof
  assume e c= [:X,Y:];
  then e c= dom pr2(X,Y) by FUNCT_3:def 5;
  hence thesis by FUNCT_3:def 1;
end;

theorem Th49:
  for X1 being Subset of X, Y1 being Subset of Y st [:X1,Y1:] <>
  {} holds pr1(X,Y).:[:X1,Y1:] = X1 & pr2(X,Y).:[:X1,Y1:] = Y1
proof
  let X1 be Subset of X, Y1 be Subset of Y;
  assume
A1: [:X1,Y1:] <> {};
  then
A2: X1 <> {};
A3: Y1 <> {} by A1;
A4: X <> {} by A2;
  now
    set y = the Element of Y1;
    let x be set;
    thus x in pr1(X,Y).:[:X1,Y1:] implies x in X1
    proof
      assume x in pr1(X,Y).:[:X1,Y1:];
      then consider u such that
A5:   u in [:X,Y:] and
A6:   u in [:X1,Y1:] & x = pr1(X,Y).u by FUNCT_2:64;
A7:   u`2 in Y by A5,MCART_1:10;
      u`1 in X1 & x = pr1(X,Y).(u`1,u`2) by A6,MCART_1:10,21;
      hence thesis by A7,FUNCT_3:def 4;
    end;
    assume
A8: x in X1;
    y in Y by A3,TARSKI:def 3;
    then
A9: x = pr1(X,Y).(x,y) by A8,FUNCT_3:def 4;
    [x,y] in [:X1,Y1:] by A3,A8,ZFMISC_1:87;
    hence x in pr1(X,Y).:[:X1,Y1:] by A4,A9,FUNCT_2:35;
  end;
  hence pr1(X,Y).:[:X1,Y1:] = X1 by TARSKI:1;
A10: Y <> {} by A3;
  now
    set x = the Element of X1;
    let y be set;
    thus y in pr2(X,Y).:[:X1,Y1:] implies y in Y1
    proof
      assume y in pr2(X,Y).:[:X1,Y1:];
      then consider u such that
A11:  u in [:X,Y:] and
A12:  u in [:X1,Y1:] & y = pr2(X,Y).u by FUNCT_2:64;
A13:  u`1 in X by A11,MCART_1:10;
      u`2 in Y1 & y = pr2(X,Y).(u`1,u`2) by A12,MCART_1:10,21;
      hence thesis by A13,FUNCT_3:def 5;
    end;
    assume
A14: y in Y1;
    x in X by A2,TARSKI:def 3;
    then
A15: y = pr2(X,Y).(x,y) by A14,FUNCT_3:def 5;
    [x,y] in [:X1,Y1:] by A2,A14,ZFMISC_1:87;
    hence y in pr2(X,Y).:[:X1,Y1:] by A10,A15,FUNCT_2:35;
  end;
  hence thesis by TARSKI:1;
end;

theorem Th50:
  for X1 being Subset of X, Y1 being Subset of Y st [:X1,Y1:] <>
  {} holds .:pr1(X,Y). [:X1,Y1:] = X1 & .:pr2(X,Y). [:X1,Y1:] = Y1
proof
  let X1 be Subset of X, Y1 be Subset of Y;
  assume
A1: [:X1,Y1:] <> {};
  thus .:pr1(X,Y). [:X1,Y1:] = pr1(X,Y).:[:X1,Y1:] by Th47
    .= X1 by A1,Th49;
  thus .:pr2(X,Y). [:X1,Y1:] = pr2(X,Y).:[:X1,Y1:] by Th48
    .= Y1 by A1,Th49;
end;

theorem
  for A being Subset of [:X,Y:], H being Subset-Family of [:X,Y:]
st for e st e in H holds e c= A & ex X1 being Subset of X, Y1 being Subset of Y
  st e =[:X1,Y1:] holds [:union(.:pr1(X,Y).:H), meet(.:pr2(X,Y).:H):] c= A
proof
  let A be Subset of [:X,Y:], H be Subset-Family of [:X,Y:] such that
A1: for e st e in H holds e c= A & ex X1 being Subset of X, Y1 being
  Subset of Y st e =[:X1,Y1:];
  let u,v;
  assume
A2: [u,v] in [:union(.:pr1(X,Y).:H), meet(.:pr2(X,Y).:H):];
  then
A3: v in meet(.:pr2(X,Y).:H) by ZFMISC_1:87;
  u in union(.:pr1(X,Y).:H) by A2,ZFMISC_1:87;
  then consider x being set such that
A4: u in x and
A5: x in .:pr1(X,Y).:H by TARSKI:def 4;
  consider y being set such that
  y in dom .:pr1(X,Y) and
A6: y in H and
A7: x = .:pr1(X,Y).y by A5,FUNCT_1:def 6;
  consider X1 being Subset of X, Y1 being Subset of Y such that
A8: y =[:X1,Y1:] by A1,A6;
A9: y <> {} by A4,A7,FUNCT_3:8;
  y in bool[:X,Y:] by A6;
  then y in bool dom pr2(X,Y) by FUNCT_3:def 5;
  then y in dom .:pr2(X,Y) by FUNCT_3:def 1;
  then .:pr2(X,Y).y in .:pr2(X,Y).:H by A6,FUNCT_1:def 6;
  then Y1 in .:pr2(X,Y).:H by A8,A9,Th50;
  then
A10: v in Y1 by A3,SETFAM_1:def 1;
  u in X1 by A4,A7,A8,A9,Th50;
  then
A11: [u,v] in y by A8,A10,ZFMISC_1:87;
  y c= A by A1,A6;
  hence thesis by A11;
end;

theorem
  for A being Subset of [:X,Y:], H being Subset-Family of [:X,Y:] st for
e st e in H holds e c= A & ex X1 being Subset of X, Y1 being Subset of Y st e =
  [:X1,Y1:] holds [:meet(.:pr1(X,Y).:H), union(.:pr2(X,Y).:H):] c= A
proof
  let A be Subset of [:X,Y:], H be Subset-Family of [:X,Y:] such that
A1: for e st e in H holds e c= A & ex X1 being Subset of X, Y1 being
  Subset of Y st e =[:X1,Y1:];
  let u,v;
  assume
A2: [u,v] in [:meet(.:pr1(X,Y).:H), union(.:pr2(X,Y).:H):];
  then
A3: u in meet(.:pr1(X,Y).:H) by ZFMISC_1:87;
  v in union(.:pr2(X,Y).:H) by A2,ZFMISC_1:87;
  then consider x being set such that
A4: v in x and
A5: x in .:pr2(X,Y).:H by TARSKI:def 4;
  consider y being set such that
  y in dom .:pr2(X,Y) and
A6: y in H and
A7: x = .:pr2(X,Y).y by A5,FUNCT_1:def 6;
  consider X1 being Subset of X, Y1 being Subset of Y such that
A8: y =[:X1,Y1:] by A1,A6;
A9: y <> {} by A4,A7,FUNCT_3:8;
  y in bool[:X,Y:] by A6;
  then y in bool dom pr1(X,Y) by FUNCT_3:def 4;
  then y in dom .:pr1(X,Y) by FUNCT_3:def 1;
  then .:pr1(X,Y).y in .:pr1(X,Y).:H by A6,FUNCT_1:def 6;
  then X1 in .:pr1(X,Y).:H by A8,A9,Th50;
  then
A10: u in X1 by A3,SETFAM_1:def 1;
  v in Y1 by A4,A7,A8,A9,Th50;
  then
A11: [u,v] in y by A8,A10,ZFMISC_1:87;
  y c= A by A1,A6;
  hence thesis by A11;
end;

theorem
  for X being set, Y being non empty set, f being Function of X,Y
  for H being Subset-Family of X holds union(.:f.:H) = f.: union H
proof
  let X be set, Y be non empty set, f be Function of X,Y;
  let H be Subset-Family of X;
  dom f = X by FUNCT_2:def 1;
  hence thesis by FUNCT_3:14;
end;

reserve X,Y,Z for non empty set;

theorem
  for X being set, a being Subset-Family of X holds union union a
  = union { union A where A is Subset of X: A in a }
proof
  let X be set, a be Subset-Family of X;
  thus union union a c= union { union A where A is Subset of X: A in a }
  proof
    let e;
    assume e in union union a;
    then consider B being set such that
A1: e in B and
A2: B in union a by TARSKI:def 4;
    consider C being set such that
A3: B in C and
A4: C in a by A2,TARSKI:def 4;
A5: union C in { union A where A is Subset of X: A in a } by A4;
    e in union C by A1,A3,TARSKI:def 4;
    hence thesis by A5,TARSKI:def 4;
  end;
  let e;
  assume e in union { union A where A is Subset of X: A in a };
  then consider c being set such that
A6: e in c and
A7: c in { union A where A is Subset of X: A in a } by TARSKI:def 4;
  consider A being Subset of X such that
A8: c = union A and
A9: A in a by A7;
  consider b being set such that
A10: e in b and
A11: b in A by A6,A8,TARSKI:def 4;
  b in union a by A9,A11,TARSKI:def 4;
  hence thesis by A10,TARSKI:def 4;
end;

theorem Th55:
  for X being set for D being Subset-Family of X st union D = X
for A being Subset of D, B being Subset of X st B = union A holds B` c= union A
  `
proof
  let X be set;
  let D be Subset-Family of X such that
A1: union D = X;
  let A be Subset of D, B be Subset of X such that
A2: B = union A;
  let e;
  assume
A3: e in B`;
  then consider u such that
A4: e in u and
A5: u in D by A1,TARSKI:def 4;
  not e in B by A3,XBOOLE_0:def 5;
  then not u in A by A2,A4,TARSKI:def 4;
  then u in A` by A5,SUBSET_1:29;
  hence thesis by A4,TARSKI:def 4;
end;

theorem
  for F being Function of X,Y, G being Function of X,Z st for x,x9
being Element of X st F.x=F.x9 holds G.x=G.x9 ex H being Function of Y,Z st H*F
  =G
proof
  let F be Function of X,Y, G be Function of X,Z;
  defpred P[set,set] means not (ex x being Element of X st $1 = F.x) or for x
  being Element of X st $1 = F.x holds $2 = G.x;
  assume
A1: for x,x9 being Element of X st F.x=F.x9 holds G.x=G.x9;
A2: now
    let e such that
    e in Y;
    now
      per cases;
      case
        ex x being Element of X st e = F.x;
        then consider x being Element of X such that
A3:     e = F.x;
        take u = G.x;
        thus u in Z & ((ex x being Element of X st e = F.x) implies ex x being
        Element of X st e = F.x & u = G.x) by A3;
      end;
      case
A4:     not ex x being Element of X st e = F.x;
        set u = the Element of Z;
        u in Z;
        hence
        ex u st u in Z & ((ex x being Element of X st e = F.x) implies ex
        x being Element of X st e = F.x & u = G.x) by A4;
      end;
    end;
    then consider u such that
A5: u in Z and
A6: (ex x being Element of X st e = F.x) implies ex x being Element of
    X st e = F.x & u = G.x;
    take u;
    thus u in Z by A5;
    thus P[e,u] by A1,A6;
  end;
  consider H being Function of Y,Z such that
A7: for e st e in Y holds P[e,H.e] from FUNCT_2:sch 1(A2);
  take H;
  now
    let x be Element of X;
    thus (H*F).x = H.(F.x) by FUNCT_2:15
      .= G.x by A7;
  end;
  hence thesis by FUNCT_2:63;
end;

theorem
  for X,Y,Z for y being Element of Y, F being (Function of X,Y), G
  being Function of Y,Z holds F"{y} c= (G*F)"{G.y}
proof
  let X,Y,Z;
  let y be Element of Y, F be (Function of X,Y), G be Function of Y,Z;
  F"{y} c= (G*F)"Im(G,y) by FUNCT_2:44;
  hence thesis by SETWISEO:8;
end;

theorem
  for F being Function of X,Y, x being Element of X, z being
  Element of Z holds [:F,id Z:].(x,z) = [F.x,z]
proof
  let F be Function of X,Y, x be Element of X, z be Element of Z;
  thus [:F,id Z:].(x,z) = [F.x, (id Z).z] by FUNCT_3:75
    .= [F.x,z] by FUNCT_1:18;
end;

theorem
  for F being Function of X,Y, A being Subset of X, B being Subset
  of Z holds [:F,id Z:].:[:A,B:] = [:F.:A,B:]
proof
  let F be Function of X,Y, A be Subset of X, B be Subset of Z;
  thus [:F,id Z:].:[:A,B:] = [:F.:A, (id Z).:B:] by FUNCT_3:72
    .= [:F.:A,B:] by FUNCT_1:92;
end;

theorem
  for F being Function of X,Y, y being Element of Y, z being
  Element of Z holds [:F,id Z:]"{[y,z]} = [:F"{y},{z}:]
proof
  let F be Function of X,Y, y be Element of Y, z be Element of Z;
  thus [:F,id Z:]"{[y,z]} = [:F,id Z:]"[:{y},{z}:] by ZFMISC_1:29
    .= [:F"{y},(id Z)"{z}:] by FUNCT_3:73
    .= [:F"{y},{z}:] by FUNCT_2:94;
end;

theorem
  for D being Subset-Family of X, A being Subset of D holds union
  A is Subset of X
proof
  let D be Subset-Family of X, A be Subset of D;
  union A c= X
  proof
    let e;
    assume e in union A;
    then ex u st e in u & u in A by TARSKI:def 4;
    then e in union D by TARSKI:def 4;
    hence thesis;
  end;
  hence thesis;
end;

theorem
  for X being set, D being a_partition of X, A,B being Subset of D
  holds union(A /\ B) = union A /\ union B
proof
  let X be set, D be a_partition of X, A,B be Subset of D;
  thus union(A/\B) c= union A /\ union B by ZFMISC_1:79;
  let e;
  assume
A1: e in union A /\ union B;
  then e in union A by XBOOLE_0:def 4;
  then consider a being set such that
A2: e in a and
A3: a in A by TARSKI:def 4;
A4: a in D by A3;
  e in union B by A1,XBOOLE_0:def 4;
  then consider b being set such that
A5: e in b and
A6: b in B by TARSKI:def 4;
A7: b in D by A6;
  not a misses b by A2,A5,XBOOLE_0:3;
  then a = b by A4,A7,Def4;
  then a in A/\B by A3,A6,XBOOLE_0:def 4;
  hence thesis by A2,TARSKI:def 4;
end;

theorem
  for D being a_partition of X, A being Subset of D, B being
  Subset of X st B = union A holds B` = union A`
proof
  let D be a_partition of X, A be Subset of D, B be Subset of X;
  assume
A1: B = union A;
  union D = X by Def4;
  hence B` c= union A` by A1,Th55;
  let e;
  assume e in union A`;
  then consider u such that
A2: e in u and
A3: u in A` by TARSKI:def 4;
A4: u in D by A3;
  assume not e in B`;
  then e in B by A2,A4,SUBSET_1:29;
  then consider v being set such that
A5: e in v and
A6: v in A by A1,TARSKI:def 4;
A7: v in D by A6;
  not u misses v by A2,A5,XBOOLE_0:3;
  then u = v by A4,A7,Def4;
  hence contradiction by A3,A6,XBOOLE_0:def 5;
end;

theorem ::Class(id X) is non-empty
  for E being Equivalence_Relation of X holds Class(E) is non empty;

registration
  let X be non empty set;
  cluster non empty for a_partition of X;
  existence
  proof

    reconsider P = Class nabla X as a_partition of X;
    take P;
    thus thesis;
  end;
end;

definition
  let X;
  let D be non empty a_partition of X;
  func proj D -> Function of X, D means
  :Def9:
  for p being Element of X holds p in it.p;
  existence
  proof
    defpred P[set,set] means $1 in $2;
A1: now
A2:   union D = X by Def4;
      let e;
      assume e in X;
      then ex u st e in u & u in D by A2,TARSKI:def 4;
      hence ex u st u in D & P[e,u];
    end;
    consider F being Function of X, D such that
A3: for e st e in X holds P[e,F.e] from FUNCT_2:sch 1(A1);
    take F;
    let p be Element of X;
    thus thesis by A3;
  end;
  correctness
  proof
    let F,G be Function of X,D such that
A4: ( for p being Element of X holds p in F.p)& for p being Element of
    X holds p in G.p;
    now
      let x be Element of X;
      x in F.x & x in G.x by A4;
      then
A5:   not F.x misses G.x by XBOOLE_0:3;
      F.x is Subset of X & G.x is Subset of X by TARSKI:def 3;
      hence F.x = G.x by A5,Def4;
    end;
    hence F = G by FUNCT_2:63;
  end;
end;

theorem Th65:
  for D being non empty a_partition of X, p being Element of X, A
  being Element of D st p in A holds A = (proj D).p
proof
  let D be non empty a_partition of X, p be Element of X, A be Element of D
  such that
A1: p in A;
  p in (proj D).p by Def9;
  then (proj D).p is Subset of X & not (proj D).p misses A by A1,TARSKI:def 3
,XBOOLE_0:3;
  hence thesis by Def4;
end;

theorem
  for D being non empty a_partition of X, p being Element of D
  holds p = proj D " {p}
proof
  let D be non empty a_partition of X, p be Element of D;
  thus p c= proj D " {p}
  proof
    let e;
    assume
A1: e in p;
    then (proj D).e = p by Th65;
    then (proj D).e in {p} by TARSKI:def 1;
    hence thesis by A1,FUNCT_2:38;
  end;
  let e;
  assume
A2: e in proj D " {p};
  then (proj D).e in {p} by FUNCT_1:def 7;
  then (proj D).e = p by TARSKI:def 1;
  hence e in p by A2,Def9;
end;

theorem
  for D being non empty a_partition of X, A being Subset of D
  holds (proj D)"A = union A
proof
  let D be non empty a_partition of X, A be Subset of D;
  thus (proj D)"A c= union A
  proof
    let e;
    assume e in (proj D)"A;
    then (proj D).e in A & e in (proj D).e by Def9,FUNCT_2:38;
    hence thesis by TARSKI:def 4;
  end;
  let e;
  assume e in union A;
  then consider u such that
A1: e in u and
A2: u in A by TARSKI:def 4;
A3: u in D by A2;
  then (proj D).e = u by A1,Th65;
  hence thesis by A1,A2,A3,FUNCT_2:38;
end;

theorem
  for D being non empty a_partition of X, W being Element of D ex
  W9 being Element of X st proj(D).W9=W
proof
  let D be non empty a_partition of X, W be Element of D;
  reconsider p = W as Subset of X;
  p <> {} by Def4;
  then consider W9 being Element of X such that
A1: W9 in p by SUBSET_1:4;
  take W9;
  thus thesis by A1,Th65;
end;

theorem
  for D being non empty a_partition of X, W being Subset of X st
for B being Subset of X st B in D & B meets W holds B c= W holds W = proj D " (
  proj D .: W)
proof
  let D be non empty a_partition of X, W be Subset of X such that
A1: for B being Subset of X st B in D & B meets W holds B c= W;
  W c= X;
  then W c= dom proj D by FUNCT_2:def 1;
  hence W c= proj D " (proj D .: W) by FUNCT_1:76;
  let e;
  assume
A2: e in proj D " (proj D .: W);
  then reconsider d = e as Element of X;
  (proj D).e in proj D .: W by A2,FUNCT_1:def 7;
  then consider c being Element of X such that
A3: c in W and
A4: (proj D).d = (proj D).c by FUNCT_2:65;
  reconsider B = (proj D).c as Subset of X by TARSKI:def 3;
  c in (proj D).c by Def9;
  then B meets W by A3,XBOOLE_0:3;
  then
A5: B c= W by A1;
  d in B by A4,Def9;
  hence thesis by A5;
end;

theorem
  for X being set, P being a_partition of X, x, a, b being set st
    x in a & a in P & x in b & b in P holds a = b
  proof
    let X be set, P be a_partition of X, x,a,b be set;
    assume that
A1: x in a and
A2: a in P and
A3: x in b and
A4: b in P;
    a meets b by A1,A3,XBOOLE_0:3;
    hence thesis by A2,A4,Def4;
  end;