environ

 vocabularies ENUMSET, RELATION, RELAT_AB, EQUIVREL;
 notations ENUMSET, RELATION, RELAT_AB;
 constructors ENUMSET, RELATION, RELAT_AB;
 definitions ENUMSET, RELATION, RELAT_AB;
 theorems ENUMSET, RELATION, RELAT_AB;

begin

theorem th1:
for X being set holds id X is reflexive
proof
  let X be set;
  let a be set;
  assume a in X;
  hence [a,a] in id X by RELAT_AB:def 6;
end;

theorem th2:
for X being set holds id X is symmetric
proof
  let X be set;
  let a,b be set;
  assume a: [a,b] in id X;
  then a in X & a=b by RELAT_AB:def 6;
  hence [b,a] in id X by a;
end;

theorem th3:
for X being set holds id X is transitive
proof
  let X be set;
  let a,b,c be set;
  assume a: [a,b] in id X & [b,c] in id X;
  then a in X & a=b & b in X & b=c by RELAT_AB:def 6;
  hence [a,c] in id X by a;
end;

registration
 let X be set;
 cluster reflexive symmetric transitive Relation of X,X;
 existence
 proof
   take id X;
   thus thesis by th1,th2,th3;
 end;
end;

definition
 let X be set;
 mode EquivalenceRelation of X is reflexive symmetric transitive Relation of X,X;
end;

definition
  let X,x be set;
  let R be EquivalenceRelation of X;
  assume x in X;
  func EqClass(R,x) means :def1:
  for y being set holds y in it iff [x,y] in R;
  correctness @proof end;
end;

theorem th4:
for X being set, x being set st x in X
for R being EquivalenceRelation of X
holds x in EqClass(R,x)
proof
  let X be set, x be set such that
  x: x in X;
  let R be EquivalenceRelation of X;
  [x,x] in R by x,RELAT_AB:def 8;
  hence thesis by x,def1;
end;

theorem th5:
for X being set, x being set st x in X
for R being EquivalenceRelation of X
holds EqClass(R,x) c= X
proof
  let X be set, x be set such that
  x: x in X;
  let R be EquivalenceRelation of X;
  let a be set;
  r: rng R c= X by RELAT_AB:def 5;
  assume a in EqClass(R,x); then
  [x,a] in R by x,def1; then
  a in rng R by RELAT_AB:def 2;
  hence a in X by r,ENUMSET:def 10;
end;

theorem th6:
for X being set, x,y being set st x in X & y in X
for R being EquivalenceRelation of X st [x,y] in R
holds EqClass(R,x) = EqClass(R,y)
proof
  let X be set, x,y be set such that
  x: x in X & y in X;
  let R be EquivalenceRelation of X;
  assume s: [x,y] in R; then
  r: [y,x] in R by RELATION:def 11;
  thus EqClass(R,x) c= EqClass(R,y)
  proof
    let a be set;
    assume a in EqClass(R,x); then
    [x,a] in R by x,def1;
    then [y,a] in R by r,RELATION:def 12;
    hence a in EqClass(R,y) by x,def1;
  end;
  thus EqClass(R,y) c= EqClass(R,x)
  proof
    let a be set;
    assume a in EqClass(R,y); then
    [y,a] in R by x,def1;
    then [x,a] in R by s,RELATION:def 12;
    hence a in EqClass(R,x) by x,def1;
  end;
end;

theorem th7:
for X being set, x,y being set st x in X & y in X
for R being EquivalenceRelation of X st not [x,y] in R
holds EqClass(R,x) /\ EqClass(R,y) = {}
proof
  let X be set, x,y be set such that
  x: x in X & y in X;
  let R be EquivalenceRelation of X;
  assume r: not [x,y] in R;
  thus EqClass(R,x) /\ EqClass(R,y) c= {}
  proof
    let a be set;
    assume a in EqClass(R,x) /\ EqClass(R,y); then
    a in EqClass(R,x) & a in EqClass(R,y) by ENUMSET:def 7; then
    [x,a] in R & [y,a] in R by def1,x; then
    [x,a] in R & [a,y] in R by RELATION:def 11;
    hence a in {} by RELATION:def 12,r;
  end;
  thus {} c= EqClass(R,x) /\ EqClass(R,y)
  proof
    let a be set;
    assume a in {};
    hence thesis by ENUMSET:def 1;
  end;
end;

definition
  let X be set;
  mode Partition of X means :def2:
  union it = X & for Y,Z being set st Y in it & Z in it & Y<>Z holds Y/\Z={};
  existence
  proof
    take {X};
    thus union {X} = X
    proof
      thus union {X} c= X
      proof
        let a be set;
        assume a in union {X}; then
        consider b being set such that
        b: a in b & b in {X} by ENUMSET:def 13;
        thus a in X by b,ENUMSET:def 3;
      end;
      thus X c= union {X}
      proof
        let a be set;
        assume a: a in X;
        X in {X} by ENUMSET:def 3;
        hence a in union {X} by a,ENUMSET:def 13;
      end;
    end;
    let Y,Z be set;
    assume a: Y in {X} & Z in {X} & Y<>Z; then
    Y = X & Z = X by ENUMSET:def 3;
    hence Y/\Z={} by a;
  end;
end;

theorem th8:
for X,Y being set, P being Partition of X
st Y in P holds Y c= X
proof
  let X,Y be set, P be Partition of X;
  assume y: Y in P;
  let a be set;
  assume a in Y;
  then a in union P by ENUMSET:def 13,y;
  hence a in X by def2;
end;


theorem th9:
for X,P being set, R being EquivalenceRelation of X holds
(for y being set holds y in P iff ex x being set st x in X & y=EqClass(R,x)) implies P is Partition of X
proof
  let X,P be set, R be EquivalenceRelation of X;
  assume a: (for y being set holds y in P iff ex x being set st x in X & y=EqClass(R,x));
  thus union P = X
  proof
    thus union P c= X
    proof
      let a be set;
      assume a in union P; then
      consider y being set such that
      y: a in y & y in P by ENUMSET:def 13;
      consider x being set such that
      x: x in X & y=EqClass(R,x) by y,a;
      y c= X by th5,x;
      hence a in X by y,ENUMSET:def 10;
    end;
    thus X c= union P
    proof
      let a be set;
      assume i: a in X; then
      e: EqClass(R,a) in P by a;
      a in EqClass(R,a) by i,th4;
      hence a in union P by e,ENUMSET:def 13;
    end;
  end;
  let Y,Z be set;
  assume Y in P; then
  consider y being set such that
  y: y in X & Y=EqClass(R,y) by a;
  assume Z in P; then
  consider z being set such that
  z: z in X & Z=EqClass(R,z) by a;
  assume n: Y<>Z; then
  not [y,z] in R by y,z,th6;
  hence Y/\Z = {} by y,z,th7;
end;

theorem th10:
for X,R being set, P being Partition of X holds
(for x being set holds x in R iff ex y,z,A being set st x=[y,z] & A in P & y in A & z in A)
implies R is EquivalenceRelation of X
proof
  let X,R be set, P be Partition of X;
  assume a:(for x being set holds x in R iff ex y,z,A being set st x=[y,z] & A in P & y in A & z in A);
  now
    let x be set;
    assume x in R; then
    consider y,z,A being set such that
    yz: x=[y,z] & A in P & y in A & z in A by a;
    thus ex y,z being set st x=[y,z] by yz;
  end;
  then reconsider S=R as Relation by RELATION:def 1;
  d: dom S c= X
  proof
    let a be set;
    assume a in dom S;
    then consider b being set such that
    b: [a,b] in S by RELAT_AB:def 1;
    consider y,z,A being set such that
    yz: [a,b]=[y,z] & A in P & y in A & z in A by a,b;
    a=y & A c= X by ENUMSET:2,yz,th8;
    hence a in X by yz,ENUMSET:def 10;
  end;
  rng S c= X
  proof
    let a be set;
    assume a in rng S;
    then consider b being set such that
    b: [b,a] in S by RELAT_AB:def 2;
    consider y,z,A being set such that
    yz: [b,a]=[y,z] & A in P & y in A & z in A by a,b;
    a=z & A c= X by ENUMSET:2,yz,th8;
    hence a in X by yz,ENUMSET:def 10;
  end;
  then reconsider S as Relation of X,X by d,RELAT_AB:def 5;
  r: S is reflexive
  proof
    let a be set;
    assume a in X; then
    a in union P by def2; then
    consider Y being set such that
    y: a in Y & Y in P by ENUMSET:def 13;
    thus [a,a] in S by a,y;
  end;
  s: S is symmetric
  proof
    let a,b be set;
    assume [a,b] in S;
    then consider y,z,A being set such that
    yz: [a,b]=[y,z] & A in P & y in A & z in A by a;
    a=y & b=z by ENUMSET:2,yz;
    hence [b,a] in S by yz,a;
  end;
  S is transitive
  proof
    let a,b,c be set;
    assume [a,b] in S;
    then consider y,z,A being set such that
    yz: [a,b]=[y,z] & A in P & y in A & z in A by a;
    e: a=y & b=z by ENUMSET:2,yz;
    assume [b,c] in S;
    then consider u,v,B being set such that
    uv: [b,c]=[u,v] & B in P & u in B & v in B by a;
    f: b=u & c = v by ENUMSET:2,uv;
    then b in A & b in B by yz,uv,e; then
    b in A/\B by ENUMSET:def 7; then
    A/\B <> {} by ENUMSET:def 1; then
    A=B by def2,uv,yz;
    hence [a,c] in S by yz,uv,a,e,f;
  end;
  hence thesis by r,s;
end;