:: Relations of Tolerance
::  by Krzysztof Hryniewiecki
::
:: Received September 20, 1990
:: 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 XBOOLE_0, RELAT_2, RELAT_1, EQREL_1, WELLORD1, ZFMISC_1,
      PARTFUN1, SUBSET_1, TARSKI, ORDINAL1, TOLER_1;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, RELSET_1, RELAT_2,
      PARTFUN1, ORDINAL1, WELLORD1, EQREL_1;
 constructors ORDINAL1, WELLORD1, EQREL_1, RELSET_1;
 registrations XBOOLE_0, SUBSET_1, RELAT_1, PARTFUN1, EQREL_1, RELSET_1;
 requirements SUBSET, BOOLE;
 definitions TARSKI, RELAT_1, RELAT_2, WELLORD1;
 theorems TARSKI, RELAT_1, RELSET_1, RELAT_2, ZFMISC_1, WELLORD1, ENUMSET1,
      ORDERS_1, EQREL_1, ORDINAL1, XBOOLE_0, XBOOLE_1, PARTFUN1, XTUPLE_0;
 schemes XBOOLE_0;

begin

reserve X,Y,Z,x,y,z for set;

registration
  cluster empty -> reflexive irreflexive symmetric antisymmetric asymmetric
    connected strongly_connected transitive for Relation;
  coherence
  proof
    let R be Relation such that
A1: R is empty;
    x in {} implies [x,x] in {};
    then {} is_reflexive_in field {} by RELAT_2:def 1;
    hence R is reflexive by A1,RELAT_2:def 9;
    {} is_irreflexive_in field {}
    proof
      let x;
      assume x in field {};
      thus thesis;
    end;
    hence R is irreflexive by A1,RELAT_2:def 10;
    thus R is symmetric
    proof
      let x,y;
      assume that
      x in field R and
      y in field R and
A2:   [x,y] in R;
      thus thesis by A1,A2;
    end;
    {} is_antisymmetric_in field {}
    proof
      let x,y;
      assume that
A3:   x in field {} and
      y in field {} and
      [x,y] in {} and
      [y,x] in {};
      thus thesis by A3;
    end;
    hence R is antisymmetric by A1,RELAT_2:def 12;
    {} is_asymmetric_in field {}
    proof
      let x,y;
      assume that
      x in field {} and
      y in field {} and
      [x,y] in {};
      thus thesis;
    end;
    hence R is asymmetric by A1,RELAT_2:def 13;
    {} is_connected_in field {}
    proof
      let x,y;
      assume that
A4:   x in field {} and
      y in field {} and
      x <> y;
      thus thesis by A4;
    end;
    hence R is connected by A1,RELAT_2:def 14;
    {} is_strongly_connected_in field {}
    proof
      let x,y;
      assume that
A5:   x in field {} and
      y in field {};
      thus thesis by A5;
    end;
    hence R is strongly_connected by A1,RELAT_2:def 15;
    {} is_transitive_in field {}
    proof
      let x,y,z;
      assume that
A6:   x in field {} and
      y in field {} and
      z in field {} and
      [x,y] in {} and
      [y,z] in {};
      thus thesis by A6;
    end;
    hence R is transitive by A1,RELAT_2:def 16;
  end;
end;

:: Total relation

notation
  let X;
  synonym Total X for nabla X;
end;

definition
  let R be Relation, Y be set;
  redefine func R |_2 Y -> Relation of Y,Y;
  coherence by XBOOLE_1:17;
end;

theorem
  rng Total X = X
proof
  for x holds x in X iff ex y st [y,x] in Total X
  proof
    let x;
    thus x in X implies ex y st [y,x] in Total X
    proof
      assume
A1:   x in X;
      take x;
      [x,x] in [:X,X:] by A1,ZFMISC_1:87;
      hence thesis by EQREL_1:def 1;
    end;
    given y such that
A2: [y,x] in Total X;
    thus thesis by A2,ZFMISC_1:87;
  end;
  hence thesis by XTUPLE_0:def 13;
end;

theorem Th2:
  for x,y st x in X & y in X holds [x,y] in Total X
proof
  let x,y;
  assume x in X & y in X;
  then [x,y] in [:X,X:] by ZFMISC_1:87;
  hence thesis by EQREL_1:def 1;
end;

theorem
  for x,y st x in field Total X & y in field Total X holds [x,y] in Total X
proof
  let x,y;
  assume x in field Total X & y in field Total X;
  then x in X & y in X by ORDERS_1:12;
  hence thesis by Th2;
end;

theorem
  Total X is strongly_connected
proof
  let x,y;
  assume x in field Total X & y in field Total X;
  then x in X & y in X by ORDERS_1:12;
  then [x,y] in [:X,X:] by ZFMISC_1:87;
  hence thesis by EQREL_1:def 1;
end;

theorem
  Total X is connected
proof
  let x,y;
  assume that
A1: x in field Total X & y in field Total X and
  x<>y;
  x in X & y in X by A1,ORDERS_1:12;
  then [x,y] in [:X,X:] by ZFMISC_1:87;
  hence thesis by EQREL_1:def 1;
end;

:: Tolerance

reserve T,R for Tolerance of X;

theorem
  for T being Tolerance of X holds rng T = X
proof
  let T be Tolerance of X;
  for x holds x in rng T iff x in X
  proof
    let x;
    x in X implies x in rng T
    proof
      field T = X by ORDERS_1:12;
      then
A1:   T is_reflexive_in X by RELAT_2:def 9;
      assume x in X;
      then [x,x] in T by A1,RELAT_2:def 1;
      hence thesis by XTUPLE_0:def 13;
    end;
    hence thesis;
  end;
  hence thesis by TARSKI:1;
end;

theorem Th7:
  for T being total reflexive Relation of X holds x in X iff [x,x] in T
proof
  let T be total reflexive Relation of X;
  thus x in X implies [x,x] in T by EQREL_1:5;
  assume
A1: [x,x] in T;
  field T = X by ORDERS_1:12;
  hence thesis by A1,RELAT_1:15;
end;

theorem
  for T being Tolerance of X holds T is_reflexive_in X
proof
  let T be Tolerance of X;
  field T = X by ORDERS_1:12;
  hence thesis by RELAT_2:def 9;
end;

theorem
  for T being Tolerance of X holds T is_symmetric_in X
proof
  let T be Tolerance of X;
  field T = X by ORDERS_1:12;
  hence thesis by RELAT_2:def 11;
end;

theorem Th10:
  for R be Relation of X,Y st R is symmetric holds R |_2 Z is symmetric
proof
  let R be Relation of X,Y;
  assume R is symmetric;
  then
A1: R is_symmetric_in field R by RELAT_2:def 11;
  now
    let x,y;
    assume that
A2: x in field(R|_2 Z) & y in field(R|_2 Z) and
A3: [x,y] in R|_2 Z;
A4: [x,y] in R by A3,XBOOLE_0:def 4;
A5: [y,x] in [:Z,Z:] by A3,ZFMISC_1:88;
    x in field R & y in field R by A2,WELLORD1:12;
    then [y,x] in R by A1,A4,RELAT_2:def 3;
    hence [y,x] in R|_2 Z by A5,XBOOLE_0:def 4;
  end;
  then R|_2 Z is_symmetric_in field(R|_2 Z) by RELAT_2:def 3;
  hence thesis by RELAT_2:def 11;
end;

definition
  let X,T;
  let Y be Subset of X;
  redefine func T |_2 Y -> Tolerance of Y;
  coherence
  proof
    now
      let x;
      assume x in Y;
      then [x,x] in [:Y,Y:] & [x,x] in T by Th7,ZFMISC_1:87;
      then [x,x] in T |_2 Y by XBOOLE_0:def 4;
      hence x in dom (T |_2 Y) by XTUPLE_0:def 12;
    end;
    then Y c= dom(T |_2 Y) by TARSKI:def 3;
    then dom(T |_2 Y) = Y by XBOOLE_0:def 10;
    hence T |_2 Y is Tolerance of Y by Th10,PARTFUN1:def 2,WELLORD1:15;
  end;
end;

theorem
  Y c= X implies T|_2 Y is Tolerance of Y
proof
  assume Y c= X;
  then reconsider Z = Y as Subset of X;
  T |_2 Z is Tolerance of Z;
  hence thesis;
end;

:: Set and Class of Tolerance

definition
  let X;
  let T be Tolerance of X;

  mode TolSet of T -> set means
    :Def1:
    for x,y st x in it & y in it holds [x,y ] in T;
  existence
  proof
    take {};
    let x,y;
    assume that
A1: x in {} and
    y in {};
    thus thesis by A1;
  end;
end;

theorem Th12:
  {} is TolSet of T
proof
  let x,y;
  assume that
A1: x in {} and
  y in {};
  thus thesis by A1;
end;

definition
  let X;
  let T be Tolerance of X;
  let IT be TolSet of T;
  attr IT is TolClass-like means
  :Def2:
  for x st not x in IT & x in X ex y st y in IT & not [x,y] in T;
end;

registration
  let X;
  let T be Tolerance of X;
  cluster TolClass-like for TolSet of T;
  existence
  proof
    defpred X[set] means $1 is TolSet of T;
    consider TS being set such that
A1: for x holds x in TS iff x in bool X & X[x] from XBOOLE_0:sch 1;
A2: TS c= bool X
    proof
      let x;
      assume x in TS;
      hence thesis by A1;
    end;
A3: for Z st Z c= TS & Z is c=-linear ex Y st Y in TS & for X1 being set
    st X1 in Z holds X1 c= Y
    proof
      let Z such that
A4:   Z c= TS and
A5:   Z is c=-linear;
      for x,y st x in union Z & y in union Z holds [x,y] in T
      proof
        let x,y;
        assume that
A6:     x in union Z and
A7:     y in union Z;
        consider Zy being set such that
A8:     y in Zy and
A9:     Zy in Z by A7,TARSKI:def 4;
        reconsider Zy as TolSet of T by A1,A4,A9;
        consider Zx being set such that
A10:    x in Zx and
A11:    Zx in Z by A6,TARSKI:def 4;
        reconsider Zx as TolSet of T by A1,A4,A11;
        Zx,Zy are_c=-comparable by A5,A11,A9,ORDINAL1:def 8;
        then Zx c= Zy or Zy c= Zx by XBOOLE_0:def 9;
        hence thesis by A10,A8,Def1;
      end;
      then
A12:  union Z is TolSet of T by Def1;
      take union Z;
      Z c= bool X by A2,A4,XBOOLE_1:1;
      then union Z c= union bool X by ZFMISC_1:77;
      then union Z c= X by ZFMISC_1:81;
      hence union Z in TS by A1,A12;
      let X1 be set;
      assume X1 in Z;
      hence thesis by ZFMISC_1:74;
    end;
    {} c= X & {} is TolSet of T by Th12,XBOOLE_1:2;
    then TS <> {} by A1;
    then consider Y such that
A13: Y in TS and
A14: for Z st Z in TS & Z <> Y holds not Y c= Z by A3,ORDERS_1:65;
    reconsider Y as TolSet of T by A1,A13;
    take Y;
    let x such that
A15: not x in Y and
A16: x in X;
    set Y1 = Y \/ {x};
A17: {x} c= X by A16,ZFMISC_1:31;
    assume
A18: for y st y in Y holds [x,y] in T;
    for y,z st y in Y1 & z in Y1 holds [y,z] in T
    proof
      let y,z;
      assume that
A19:  y in Y1 and
A20:  z in Y1;
      y in Y or y in {x} by A19,XBOOLE_0:def 3;
      then
A21:  y in Y or y = x by TARSKI:def 1;
      z in Y or z in {x} by A20,XBOOLE_0:def 3;
      then
A22:  z in Y or z = x by TARSKI:def 1;
      assume
A23:  not [y,z] in T;
      then not [z,y] in T by EQREL_1:6;
      hence contradiction by A16,A18,A21,A22,A23,Def1,Th7;
    end;
    then
A24: Y1 is TolSet of T by Def1;
A25: Y1 <> Y
    proof
A26:  x in {x} by TARSKI:def 1;
      assume Y1 = Y;
      hence contradiction by A15,A26,XBOOLE_0:def 3;
    end;
    Y in bool X by A1,A13;
    then Y1 c= X by A17,XBOOLE_1:8;
    then Y1 in TS by A1,A24;
    hence contradiction by A14,A25,XBOOLE_1:7;
  end;
end;

definition
  let X;
  let T be Tolerance of X;
  mode TolClass of T is TolClass-like TolSet of T;
end;

theorem
  for T being Tolerance of X st {} is TolClass of T holds T={}
proof
  let T be Tolerance of X;
  assume {} is TolClass of T;
  then reconsider 00 = {} as TolClass of T;
  assume T <> {};
  then consider x,y such that
A1: [x,y] in T by RELAT_1:37;
  x in X by A1,ZFMISC_1:87;
  then ex z st z in 00 & not [x,z] in T by Def2;
  hence contradiction;
end;

theorem
  {} is Tolerance of {} by RELSET_1:12;

theorem Th15:
  for x,y st [x,y] in T holds {x,y} is TolSet of T
proof
  let x,y;
  assume
A1: [x,y] in T;
  then
A2: x in X & y in X by ZFMISC_1:87;
  for a,b being set st a in {x,y} & b in {x,y} holds [a,b] in T
  proof
    let a,b be set;
    assume that
A3: a in {x,y} and
A4: b in {x,y};
A5: b = x or b = y by A4,TARSKI:def 2;
    a = x or a = y by A3,TARSKI:def 2;
    hence thesis by A1,A2,A5,Th7,EQREL_1:6;
  end;
  hence thesis by Def1;
end;

theorem
  for x st x in X holds {x} is TolSet of T
proof
  let x;
  assume x in X;
  then [x,x] in T by Th7;
  then {x,x} is TolSet of T by Th15;
  hence thesis by ENUMSET1:29;
end;

theorem
  for Y,Z st Y is TolSet of T holds Y /\ Z is TolSet of T
proof
  let Y,Z such that
A1: Y is TolSet of T;
  let x,y;
  assume x in Y /\ Z & y in Y /\ Z;
  then x in Y & y in Y by XBOOLE_0:def 4;
  hence thesis by A1,Def1;
end;

theorem Th18:
  Y is TolSet of T implies Y c= X
proof
  assume
A1: Y is TolSet of T;
  let x;
  assume x in Y;
  then [x,x] in T by A1,Def1;
  hence thesis by Th7;
end;

theorem Th19:
  for Y being TolSet of T ex Z being TolClass of T st Y c= Z
proof
  let Y be TolSet of T;
  defpred X[set] means $1 is TolSet of T & ex Z st $1=Z & Y c= Z;
  consider TS being set such that
A1: for x holds x in TS iff x in bool X & X[x] from XBOOLE_0:sch 1;
A2: for x being set holds x in TS iff x in bool X & x is TolSet of T & Y c= x
  proof
    let x be set;
    thus x in TS implies x in bool X & x is TolSet of T & Y c= x
    proof
      assume
A3:   x in TS;
      hence x in bool X & x is TolSet of T by A1;
      ex Z st x=Z & Y c= Z by A1,A3;
      hence thesis;
    end;
    thus thesis by A1;
  end;
  Y c= X by Th18;
  then
A4: TS <> {} by A2;
A5: TS c= bool X
  proof
    let x;
    assume x in TS;
    hence thesis by A1;
  end;
  for Z st Z c= TS & Z is c=-linear ex Y st Y in TS & for X1 being set st
  X1 in Z holds X1 c= Y
  proof
    let Z such that
A6: Z c= TS and
A7: Z is c=-linear;
A8: for x,y st x in union Z & y in union Z holds [x,y] in T
    proof
      let x,y;
      assume that
A9:   x in union Z and
A10:  y in union Z;
      consider Zy being set such that
A11:  y in Zy and
A12:  Zy in Z by A10,TARSKI:def 4;
      reconsider Zy as TolSet of T by A1,A6,A12;
      consider Zx being set such that
A13:  x in Zx and
A14:  Zx in Z by A9,TARSKI:def 4;
      reconsider Zx as TolSet of T by A1,A6,A14;
      Zx, Zy are_c=-comparable by A7,A14,A12,ORDINAL1:def 8;
      then Zx c= Zy or Zy c= Zx by XBOOLE_0:def 9;
      hence thesis by A13,A11,Def1;
    end;
A15: Z <> {} implies thesis
    proof
      assume
A16:  Z <> {};
A17:  Y c= union Z
      proof
        set y = the Element of Z;
        y in TS by A6,A16,TARSKI:def 3;
        then
A18:    Y c= y by A2;
        let x;
        assume x in Y;
        hence thesis by A16,A18,TARSKI:def 4;
      end;
      Z c= bool X by A5,A6,XBOOLE_1:1;
      then union Z c= union bool X by ZFMISC_1:77;
      then
A19:  union Z c= X by ZFMISC_1:81;
      take union Z;
      union Z is TolSet of T by A8,Def1;
      hence union Z in TS by A2,A19,A17;
      let X1 be set;
      assume X1 in Z;
      hence thesis by ZFMISC_1:74;
    end;
    Z = {} implies thesis
    proof
      set Y = the Element of TS;
      assume
A20:  Z = {};
      take Y;
      thus Y in TS by A4;
      let X1 be set;
      assume X1 in Z;
      hence thesis by A20;
    end;
    hence thesis by A15;
  end;
  then consider Z1 being set such that
A21: Z1 in TS and
A22: for Z st Z in TS & Z<>Z1 holds not Z1 c= Z by A4,ORDERS_1:65;
  reconsider Z1 as TolSet of T by A1,A21;
  Z1 is TolClass of T
  proof
    assume not thesis;
    then consider x such that
A23: not x in Z1 and
A24: x in X and
A25: for y st y in Z1 holds [x,y] in T by Def2;
    set Y1 = Z1 \/ {x};
A26: {x} c= X by A24,ZFMISC_1:31;
    for y,z st y in Y1 & z in Y1 holds [y,z] in T
    proof
      let y,z;
      assume that
A27:  y in Y1 and
A28:  z in Y1;
      y in Z1 or y in {x} by A27,XBOOLE_0:def 3;
      then
A29:  y in Z1 or y = x by TARSKI:def 1;
      z in Z1 or z in {x} by A28,XBOOLE_0:def 3;
      then
A30:  z in Z1 or z = x by TARSKI:def 1;
      assume
A31:  not [y,z] in T;
      then not [z,y] in T by EQREL_1:6;
      hence contradiction by A24,A25,A29,A30,A31,Def1,Th7;
    end;
    then
A32: Y1 is TolSet of T by Def1;
    Y c= Z1 & Z1 c= Y1 by A2,A21,XBOOLE_1:7;
    then
A33: Y c= Y1 by XBOOLE_1:1;
A34: Y1 <> Z1
    proof
A35:  x in {x} by TARSKI:def 1;
      assume Y1 = Z1;
      hence contradiction by A23,A35,XBOOLE_0:def 3;
    end;
    Z1 in bool X by A1,A21;
    then Y1 c= X by A26,XBOOLE_1:8;
    then Y1 in TS by A2,A32,A33;
    hence contradiction by A22,A34,XBOOLE_1:7;
  end;
  then reconsider Z1 as TolClass of T;
  take Z1;
  thus thesis by A2,A21;
end;

theorem Th20:
  for x,y st [x,y] in T ex Z being TolClass of T st x in Z & y in Z
proof
  let x,y;
  assume
A1: [x,y] in T;
  then
A2: x in X & y in X by ZFMISC_1:87;
  for a,b being set st a in {x,y} & b in {x,y} holds [a,b] in T
  proof
    let a,b be set;
    assume that
A3: a in {x,y} and
A4: b in {x,y};
A5: b = x or b = y by A4,TARSKI:def 2;
    a = x or a = y by A3,TARSKI:def 2;
    hence thesis by A1,A2,A5,Th7,EQREL_1:6;
  end;
  then reconsider PS = {x,y} as TolSet of T by Def1;
  consider Z being TolClass of T such that
A6: PS c= Z by Th19;
  take Z;
  x in {x,y} by TARSKI:def 2;
  hence x in Z by A6;
  y in {x,y} by TARSKI:def 2;
  hence thesis by A6;
end;

theorem Th21:
  for x st x in X ex Z being TolClass of T st x in Z
proof
  let x;
  assume x in X;
  then [x,x] in T by Th7;
  then ex Z being TolClass of T st x in Z & x in Z by Th20;
  hence thesis;
end;

theorem
  T c= Total X
proof
  let x,y;
  assume [x,y] in T;
  then [x,y] in [:X,X:];
  hence thesis by EQREL_1:def 1;
end;

theorem
  id X c= T
proof
  let x,y;
  assume [x,y] in id X;
  then x in X & x = y by RELAT_1:def 10;
  hence thesis by Th7;
end;

scheme
  ToleranceEx{A() -> set,P[set,set]}: ex T being Tolerance of A() st for x,y
  st x in A() & y in A() holds [x,y] in T iff P[x,y]
provided
A1: for x st x in A() holds P[x,x] and
A2: for x,y st x in A() & y in A() & P[x,y] holds P[y,x]
proof
  defpred X[set] means ex y,z st $1 = [y,z] & P[y,z];
  consider T being set such that
A3: for x holds x in T iff x in [:A(),A():] & X[x] from XBOOLE_0:sch 1;
  for x st x in T holds x in [:A(),A():] by A3;
  then reconsider T as Relation of A(),A() by TARSKI:def 3;
A4: field T c= A() \/ A() by RELSET_1:8;
  for x st x in field T holds [x,x] in T
  proof
    let x;
    assume x in field T;
    then [x,x] in [:A(),A():] & P[x,x] by A1,A4,ZFMISC_1:87;
    hence thesis by A3;
  end;
  then
A5: T is_reflexive_in field T by RELAT_2:def 1;
  for x,y st x in field T & y in field T & [x,y] in T holds [y,x] in T
  proof
    let x,y such that
A6: x in field T & y in field T and
A7: [x,y] in T;
    x in A() & y in A() & P[x,y]
    proof
      thus x in A() & y in A() by A4,A6;
      consider a,b being set such that
A8:   [x,y] = [a,b] and
A9:   P[a,b] by A3,A7;
      x = a by A8,XTUPLE_0:1;
      hence thesis by A8,A9,XTUPLE_0:1;
    end;
    then [y,x] in [:A(),A():] & P[y,x] by A2,ZFMISC_1:87;
    hence thesis by A3;
  end;
  then
A10: T is_symmetric_in field T by RELAT_2:def 3;
  for x st x in A() holds x in dom T
  proof
    let x;
    assume x in A();
    then [x,x] in [:A(),A():] & P[x,x] by A1,ZFMISC_1:87;
    then [x,x] in T by A3;
    hence thesis by XTUPLE_0:def 12;
  end;
  then A() c= dom T by TARSKI:def 3;
  then dom T = A() by XBOOLE_0:def 10;
  then reconsider T as Tolerance of A() by A5,A10,PARTFUN1:def 2,RELAT_2:def 9
,def 11;
  take T;
  let x,y;
  assume
A11: x in A() & y in A();
  thus [x,y] in T implies P[x,y]
  proof
    assume [x,y] in T;
    then consider a,b being set such that
A12: [x,y] = [a,b] and
A13: P[a,b] by A3;
    x = a by A12,XTUPLE_0:1;
    hence thesis by A12,A13,XTUPLE_0:1;
  end;
  assume
A14: P[x,y];
  [x,y] in [:A(),A():] by A11,ZFMISC_1:87;
  hence thesis by A3,A14;
end;

theorem
  for Y ex T being Tolerance of union Y st for Z st Z in Y holds Z is
  TolSet of T
proof
  let Y;
  defpred X[set,set] means ex Z st Z in Y & $1 in Z & $2 in Z;
A1: for x st x in union Y holds X[x,x]
  proof
    let x;
    assume x in union Y;
    then ex Z st x in Z & Z in Y by TARSKI:def 4;
    hence thesis;
  end;
A2: for x,y st x in union Y & y in union Y & X[x,y] holds X[y,x];
  consider T being Tolerance of union Y such that
A3: for x,y st x in union Y & y in union Y holds [x,y] in T iff X[x,y]
  from ToleranceEx(A1,A2);
  take T;
  let Z such that
A4: Z in Y;
  for x,y st x in Z & y in Z holds [x,y] in T
  proof
    let x,y;
    assume
A5: x in Z & y in Z;
    then x in union Y & y in union Y by A4,TARSKI:def 4;
    hence thesis by A3,A4,A5;
  end;
  hence thesis by Def1;
end;

theorem
  for Y being set for T,R being Tolerance of union Y st (for x,y holds [
x,y] in T iff ex Z st Z in Y & x in Z & y in Z) & (for x,y holds [x,y] in R iff
  ex Z st Z in Y & x in Z & y in Z) holds T = R
proof
  let Y be set;
  let T,R be Tolerance of union Y such that
A1: for x,y holds [x,y] in T iff ex Z st Z in Y & x in Z & y in Z and
A2: for x,y holds [x,y] in R iff ex Z st Z in Y & x in Z & y in Z;
  for x,y holds [x,y] in T iff [x,y] in R
  proof
    let x,y;
    thus [x,y] in T implies [x,y] in R
    proof
      assume [x,y] in T;
      then ex Z st Z in Y & x in Z & y in Z by A1;
      hence thesis by A2;
    end;
    assume [x,y] in R;
    then ex Z st Z in Y & x in Z & y in Z by A2;
    hence thesis by A1;
  end;
  hence thesis by RELAT_1:def 2;
end;

theorem Th26:
  for T,R being Tolerance of X st for Z holds Z is TolClass of T
  iff Z is TolClass of R holds T = R
proof
  let T,R be Tolerance of X;
  assume
A1: for Z holds Z is TolClass of T iff Z is TolClass of R;
  for x,y holds [x,y] in T iff [x,y] in R
  proof
    let x,y;
    thus [x,y] in T implies [x,y] in R
    proof
      assume [x,y] in T;
      then consider Z being TolClass of T such that
A2:   x in Z & y in Z by Th20;
      reconsider Z as TolClass of R by A1;
      Z is TolSet of R;
      hence thesis by A2,Def1;
    end;
    assume [x,y] in R;
    then consider Z being TolClass of R such that
A3: x in Z & y in Z by Th20;
    reconsider Z as TolClass of T by A1;
    Z is TolSet of T;
    hence thesis by A3,Def1;
  end;
  hence thesis by RELAT_1:def 2;
end;

:: Tolerance neighbourhood

notation
  let X, Y;
  let T be Relation of X, Y;
  let x;
  synonym neighbourhood (x, T) for Class (T,x);
end;

theorem Th27:
  for y being set holds y in neighbourhood(x,T) iff [x,y] in T
proof
  let y be set;
  hereby
    assume y in neighbourhood(x,T);
    then [y,x] in T by EQREL_1:19;
    hence [x,y] in T by EQREL_1:6;
  end;
  assume [x,y] in T;
  then [y,x] in T by EQREL_1:6;
  hence thesis by EQREL_1:19;
end;

theorem
  for Y st for Z being set holds Z in Y iff x in Z & Z is TolClass of T
  holds neighbourhood(x,T) = union Y
proof
  let Y such that
A1: for Z being set holds Z in Y iff x in Z & Z is TolClass of T;
  for y holds y in neighbourhood(x,T) iff y in union Y
  proof
    let y;
    thus y in neighbourhood(x,T) implies y in union Y
    proof
      assume y in neighbourhood(x,T);
      then [x,y] in T by Th27;
      then consider Z being TolClass of T such that
A2:   x in Z and
A3:   y in Z by Th20;
      Z in Y by A1,A2;
      hence thesis by A3,TARSKI:def 4;
    end;
    assume y in union Y;
    then consider Z such that
A4: y in Z and
A5: Z in Y by TARSKI:def 4;
    reconsider Z as TolClass of T by A1,A5;
    x in Z by A1,A5;
    then [x,y] in T by A4,Def1;
    hence thesis by Th27;
  end;
  hence thesis by TARSKI:1;
end;

theorem
  for Y st for Z holds Z in Y iff x in Z & Z is TolSet of T holds
  neighbourhood(x,T) = union Y
proof
  let Y such that
A1: for Z holds Z in Y iff x in Z & Z is TolSet of T;
  for y holds y in neighbourhood(x,T) iff y in union Y
  proof
    let y;
    thus y in neighbourhood(x,T) implies y in union Y
    proof
      assume y in neighbourhood(x,T);
      then [x,y] in T by Th27;
      then consider Z being TolClass of T such that
A2:   x in Z and
A3:   y in Z by Th20;
      Z in Y by A1,A2;
      hence thesis by A3,TARSKI:def 4;
    end;
    assume y in union Y;
    then consider Z such that
A4: y in Z and
A5: Z in Y by TARSKI:def 4;
    reconsider Z as TolSet of T by A1,A5;
    x in Z by A1,A5;
    then [x,y] in T by A4,Def1;
    hence thesis by Th27;
  end;
  hence thesis by TARSKI:1;
end;

:: Family of sets and classes of proximity

definition
  let X;
  let T be Tolerance of X;

  func TolSets T -> set means
  :Def3:
  for Y holds Y in it iff Y is TolSet of T;
  existence
  proof
    defpred X[set] means $1 is TolSet of T;
    consider Z being set such that
A1: x in Z iff x in bool X & X[x] from XBOOLE_0:sch 1;
    take Z;
    let Y;
    thus Y in Z implies Y is TolSet of T by A1;
    assume
A2: Y is TolSet of T;
    for x holds x in Y implies x in X
    proof
      let x;
      assume x in Y;
      then [x,x] in T by A2,Def1;
      hence thesis by ZFMISC_1:87;
    end;
    then Y c= X by TARSKI:def 3;
    hence thesis by A1,A2;
  end;
  uniqueness
  proof
    defpred P[set] means $1 is TolSet of T;
    let Z1,Z2 be set such that
A3: for Y holds Y in Z1 iff P[Y] and
A4: for Y holds Y in Z2 iff P[Y];
    Z1 = Z2 from XBOOLE_0:sch 2 (A3, A4);
    hence thesis;
  end;
  func TolClasses T -> set means
  :Def4:
  for Y holds Y in it iff Y is TolClass of T;
  existence
  proof
    defpred X[set] means $1 is TolClass of T;
    consider Z being set such that
A5: x in Z iff x in bool X & X[x] from XBOOLE_0:sch 1;
    take Z;
    let Y;
    thus Y in Z implies Y is TolClass of T by A5;
    assume
A6: Y is TolClass of T;
    for x holds x in Y implies x in X
    proof
      let x;
      assume x in Y;
      then [x,x] in T by A6,Def1;
      hence thesis by ZFMISC_1:87;
    end;
    then Y c= X by TARSKI:def 3;
    hence thesis by A5,A6;
  end;
  uniqueness
  proof
    defpred P[set] means $1 is TolClass of T;
    let C1,C2 be set such that
A7: for Y holds Y in C1 iff P[Y] and
A8: for Y holds Y in C2 iff P[Y];
    C1 = C2 from XBOOLE_0:sch 2 (A7, A8);
    hence thesis;
  end;
end;

theorem
  TolClasses R c= TolClasses T implies R c= T
proof
  assume
A1: TolClasses R c= TolClasses T;
  let x,y;
  assume [x,y] in R;
  then consider Z being TolClass of R such that
A2: x in Z & y in Z by Th20;
  Z in TolClasses R by Def4;
  then Z is TolSet of T by A1,Def4;
  hence thesis by A2,Def1;
end;

theorem
  for T,R being Tolerance of X st TolClasses T = TolClasses R holds T = R
proof
  let T,R be Tolerance of X;
  assume
A1: TolClasses T = TolClasses R;
  for Z holds Z is TolClass of T iff Z is TolClass of R
  proof
    let Z;
    Z is TolClass of T iff Z in TolClasses R by A1,Def4;
    hence thesis by Def4;
  end;
  hence thesis by Th26;
end;

theorem
  union TolClasses T = X
proof
  for x holds x in union TolClasses T iff x in X
  proof
    let x;
    thus x in union TolClasses T implies x in X
    proof
      assume x in union TolClasses T;
      then consider Z such that
A1:   x in Z and
A2:   Z in TolClasses T by TARSKI:def 4;
      Z is TolSet of T by A2,Def4;
      then Z c= X by Th18;
      hence thesis by A1;
    end;
    assume x in X;
    then consider Z being TolClass of T such that
A3: x in Z by Th21;
    Z in TolClasses T by Def4;
    hence thesis by A3,TARSKI:def 4;
  end;
  hence thesis by TARSKI:1;
end;

theorem
  union TolSets T = X
proof
  for x holds x in union TolSets T iff x in X
  proof
    let x;
    thus x in union TolSets T implies x in X
    proof
      assume x in union TolSets T;
      then consider Z such that
A1:   x in Z and
A2:   Z in TolSets T by TARSKI:def 4;
      Z is TolSet of T by A2,Def3;
      then Z c= X by Th18;
      hence thesis by A1;
    end;
    assume x in X;
    then consider Z being TolClass of T such that
A3: x in Z by Th21;
    Z in TolSets T by Def3;
    hence thesis by A3,TARSKI:def 4;
  end;
  hence thesis by TARSKI:1;
end;

theorem
  (for x st x in X holds neighbourhood(x,T) is TolSet of T) implies T is
  transitive
proof
  assume
A1: for x st x in X holds neighbourhood(x,T) is TolSet of T;
A2: field T = X by ORDERS_1:12;
  for x,y,z st x in field T & y in field T & z in field T & [x,y] in T & [
  y,z] in T holds [x,z] in T
  proof
    let x,y,z;
    assume that
    x in field T and
A3: y in field T and
    z in field T and
A4: [x,y] in T and
A5: [y,z] in T;
    reconsider N = neighbourhood(y,T) as TolSet of T by A2,A1,A3;
    [y,x] in T by A4,EQREL_1:6;
    then
A6: x in N by Th27;
    z in N by A5,Th27;
    hence thesis by A6,Def1;
  end;
  then T is_transitive_in field T by RELAT_2:def 8;
  hence thesis by RELAT_2:def 16;
end;

theorem
  T is transitive implies for x st x in X holds neighbourhood(x,T) is
  TolClass of T
proof
  assume
A1: T is transitive;
  let x;
  assume
A2: x in X;
  set N = Class(T,x);
  field T = X by ORDERS_1:12;
  then
A3: T is_transitive_in X by A1,RELAT_2:def 16;
  for y,z st y in N & z in N holds [y,z] in T
  proof
    let y,z such that
A4: y in N and
A5: z in N;
    [x,y] in T by A4,Th27;
    then
A6: [y,x] in T by EQREL_1:6;
    [x,z] in T by A5,Th27;
    hence thesis by A3,A2,A4,A5,A6,RELAT_2:def 8;
  end;
  then reconsider Z = N as TolSet of T by Def1;
  for x st not x in Z & x in X ex y st y in Z & not [x,y] in T
  proof
    let y such that
A7: not y in Z and
    y in X;
A8: x in Z by A2,EQREL_1:20;
    assume for z st z in Z holds [y,z] in T;
    then [y,x] in T by A8;
    then [x,y] in T by EQREL_1:6;
    hence contradiction by A7,Th27;
  end;
  hence thesis by Def2;
end;

theorem
  for x for Y being TolClass of T st x in Y holds Y c= neighbourhood(x,T )
proof
  let x;
  let Y be TolClass of T such that
A1: x in Y;
  for y st y in Y holds y in neighbourhood(x,T)
  proof
    let y;
    assume y in Y;
    then [x,y] in T by A1,Def1;
    hence thesis by Th27;
  end;
  hence thesis by TARSKI:def 3;
end;

theorem
  TolSets R c= TolSets T iff R c= T
proof
  thus TolSets R c= TolSets T implies R c= T
  proof
    assume
A1: TolSets R c= TolSets T;
    let x,y;
    assume [x,y] in R;
    then consider Z being TolClass of R such that
A2: x in Z & y in Z by Th20;
    Z in TolSets R by Def3;
    then Z is TolSet of T by A1,Def3;
    hence thesis by A2,Def1;
  end;
  assume
A3: R c= T;
  let x;
  assume x in TolSets R;
  then reconsider Z = x as TolSet of R by Def3;
  for x,y st x in Z & y in Z holds [x,y] in T
  proof
    let x,y;
    assume x in Z & y in Z;
    then [x,y] in R by Def1;
    hence thesis by A3;
  end;
  then Z is TolSet of T by Def1;
  hence thesis by Def3;
end;

theorem
  TolClasses T c= TolSets T
proof
  let x;
  assume x in TolClasses T;
  then x is TolSet of T by Def4;
  hence thesis by Def3;
end;

theorem
  (for x st x in X holds neighbourhood(x,R) c= neighbourhood(x,T))
  implies R c= T
proof
  assume
A1: for x st x in X holds neighbourhood(x,R) c= neighbourhood(x,T);
  let x,y;
  assume
A2: [x,y] in R;
  then x in X by ZFMISC_1:87;
  then
A3: neighbourhood(x,R) c= neighbourhood(x,T) by A1;
  y in neighbourhood(x,R) by A2,Th27;
  hence thesis by A3,Th27;
end;

theorem
  T c= T*T
proof
  let x,y;
  assume
A1: [x,y] in T;
  then y in X by ZFMISC_1:87;
  then [y,y] in T by Th7;
  hence thesis by A1,RELAT_1:def 8;
end;