toler_1.miz



    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;

         {} is_reflexive_in ( field {} );

        hence R is reflexive by A1;

         {} is_irreflexive_in ( field {} );

        hence R is irreflexive by A1;

        thus R is symmetric

        proof

          let x,y be object;

          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 {} );

        hence R is antisymmetric by A1;

         {} is_asymmetric_in ( field {} );

        hence R is asymmetric by A1;

         {} is_connected_in ( field {} );

        hence R is connected by A1;

         {} is_strongly_connected_in ( field {} );

        hence R is strongly_connected by A1;

         {} is_transitive_in ( field {} );

        hence R is transitive by A1;

      end;

    end

    notation

      let X;

      synonym Total X for nabla X;

    end

    definition

      let R be Relation, Y be set;

      :: original: |_2

      redefine

      func R |_2 Y -> Relation of Y, Y ;

      coherence by XBOOLE_1: 17;

    end

    theorem :: TOLER_1:1

    ( rng ( Total X)) = X

    proof

      for x be object holds x in X iff ex y be object st [y, x] in ( Total X)

      proof

        let x be object;

        thus x in X implies ex y be object 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;

        thus thesis by ZFMISC_1: 87;

      end;

      hence thesis by XTUPLE_0:def 13;

    end;

    theorem :: TOLER_1:2

    

     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 :: TOLER_1:3

    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 :: TOLER_1:4

    ( Total X) is strongly_connected

    proof

      let x,y be object;

      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 :: TOLER_1:5

    ( Total X) is connected

    proof

      let x,y be object;

      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;

    reserve T,R for Tolerance of X;

    theorem :: TOLER_1:6

    for T be Tolerance of X holds ( rng T) = X

    proof

      let T be Tolerance of X;

      for x be object holds x in ( rng T) iff x in X

      proof

        let x be object;

        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;

          hence thesis by XTUPLE_0:def 13;

        end;

        hence thesis;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: TOLER_1:7

    

     Th7: for x be object holds for T be total reflexive Relation of X holds x in X iff [x, x] in T

    proof

      let x be object;

      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 :: TOLER_1:8

    for T be 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 :: TOLER_1:9

    for T be 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 :: TOLER_1:10

    

     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);

      now

        let x,y be object;

        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;

        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));

      hence thesis;

    end;

    definition

      let X, T;

      let Y be Subset of X;

      :: original: |_2

      redefine

      func T |_2 Y -> Tolerance of Y ;

      coherence

      proof

        now

          let x be object;

          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));

        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 :: TOLER_1:11

    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;

    definition

      let X;

      let T be Tolerance of X;

      :: TOLER_1:def1

      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 :: TOLER_1:12

    

     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;

      :: TOLER_1:def2

      attr IT is TolClass-like means

      : Def2: for x st not x in IT & x in X holds 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 be set such that

         A1: for x holds x in TS iff x in ( bool X) & X[x] from XFAMILY:sch 1;

        

         A2: TS c= ( bool X) by A1;

        

         A3: for Z st Z c= TS & Z is c=-linear holds ex Y st Y in TS & for X1 be 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 be 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 be 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;

          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;

        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 :: TOLER_1:13

    for T be Tolerance of X st {} is TolClass of T holds T = {}

    proof

      let T be Tolerance of X;

      assume {} is TolClass of T;

      then

      reconsider O0 = {} as TolClass of T;

      assume T <> {} ;

      then

      consider x,y be object such that

       A1: [x, y] in T;

      x in X by A1, ZFMISC_1: 87;

      then ex z st z in O0 & not [x, z] in T by Def2;

      hence contradiction;

    end;

    theorem :: TOLER_1:14

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

    theorem :: TOLER_1:15

    

     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 be 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 :: TOLER_1:16

    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 :: TOLER_1:17

    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 :: TOLER_1:18

    

     Th18: Y is TolSet of T implies Y c= X

    proof

      assume

       A1: Y is TolSet of T;

      let x be object;

      assume x in Y;

      then [x, x] in T by A1, Def1;

      hence thesis by Th7;

    end;

    theorem :: TOLER_1:19

    

     Th19: for Y be TolSet of T holds ex Z be 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 be set such that

       A1: for x holds x in TS iff x in ( bool X) & X[x] from XFAMILY:sch 1;

      

       A2: for x be 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) by A1;

      for Z st Z c= TS & Z is c=-linear holds ex Y st Y in TS & for X1 be 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 be 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 be 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;

            then

             A18: Y c= y by A2;

            let x be object;

            assume x in Y;

            hence thesis by A16, A18, TARSKI:def 4;

          end;

          Z c= ( bool X) by A5, A6;

          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 be 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;

        

         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 :: TOLER_1:20

    

     Th20: for x,y be object st [x, y] in T holds ex Z be TolClass of T st x in Z & y in Z

    proof

      let x,y be object;

      assume

       A1: [x, y] in T;

      then

       A2: x in X & y in X by ZFMISC_1: 87;

      for a,b be 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 be 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 :: TOLER_1:21

    

     Th21: for x st x in X holds ex Z be TolClass of T st x in Z

    proof

      let x;

      assume x in X;

      then [x, x] in T by Th7;

      then ex Z be TolClass of T st x in Z & x in Z by Th20;

      hence thesis;

    end;

    theorem :: TOLER_1:22

    T c= ( Total X)

    proof

      let x,y be object;

      assume [x, y] in T;

      then [x, y] in [:X, X:];

      hence thesis by EQREL_1:def 1;

    end;

    theorem :: TOLER_1:23

    ( id X) c= T

    proof

      let x,y be object;

      assume [x, y] in ( id X);

      then x in X & x = y by RELAT_1:def 10;

      hence thesis by Th7;

    end;

    scheme :: TOLER_1:sch1

    ToleranceEx { A() -> set , P[ object, object] } :

ex T be 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];

      defpred X[ object] means ex y,z be object st $1 = [y, z] & P[y, z];

      consider T be set such that

       A3: for x be object holds x in T iff x in [:A(), A():] & X[x] from XBOOLE_0:sch 1;

      for x be object 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 be object st x in ( field T) holds [x, x] in T

      proof

        let x be object;

        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);

      for x,y be object st x in ( field T) & y in ( field T) & [x, y] in T holds [y, x] in T

      proof

        let x,y be object 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 be object 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);

      for x be object st x in A() holds x in ( dom T)

      proof

        let x be object;

        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);

      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, RELAT_2: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 be object 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 :: TOLER_1:24

    for Y holds ex T be 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 be 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 :: TOLER_1:25

    for Y be set holds for T,R be Tolerance of ( union Y) st (for x,y be object holds [x, y] in T iff ex Z st Z in Y & x in Z & y in Z) & (for x,y be object 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 be object holds [x, y] in T iff ex Z st Z in Y & x in Z & y in Z and

       A2: for x,y be object holds [x, y] in R iff ex Z st Z in Y & x in Z & y in Z;

      for x,y be object holds [x, y] in T iff [x, y] in R

      proof

        let x,y be object;

        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;

    end;

    theorem :: TOLER_1:26

    

     Th26: for T,R be 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 be object holds [x, y] in T iff [x, y] in R

      proof

        let x,y be object;

        thus [x, y] in T implies [x, y] in R

        proof

          assume [x, y] in T;

          then

          consider Z be 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 be 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;

    end;

    notation

      let X, Y;

      let T be Relation of X, Y;

      let x be object;

      synonym neighbourhood (x,T) for Class (T,x);

    end

    theorem :: TOLER_1:27

    

     Th27: for x,y be object holds y in ( neighbourhood (x,T)) iff [x, y] in T

    proof

      let x,y be object;

      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 :: TOLER_1:28

    for Y st for Z be 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 be set holds Z in Y iff x in Z & Z is TolClass of T;

      for y be object holds y in ( neighbourhood (x,T)) iff y in ( union Y)

      proof

        let y be object;

        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 be 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: 2;

    end;

    theorem :: TOLER_1:29

    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 be object holds y in ( neighbourhood (x,T)) iff y in ( union Y)

      proof

        let y be object;

        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 be 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: 2;

    end;

    definition

      let X;

      let T be Tolerance of X;

      :: TOLER_1:def3

      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 be set such that

         A1: x in Z iff x in ( bool X) & X[x] from XFAMILY: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 be object holds x in Y implies x in X

        proof

          let x be object;

          assume x in Y;

          then [x, x] in T by A2, Def1;

          hence thesis by ZFMISC_1: 87;

        end;

        then Y c= X;

        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 XFAMILY:sch 2( A3, A4);

        hence thesis;

      end;

      :: TOLER_1:def4

      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 be set such that

         A5: x in Z iff x in ( bool X) & X[x] from XFAMILY: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 be object holds x in Y implies x in X

        proof

          let x be object;

          assume x in Y;

          then [x, x] in T by A6, Def1;

          hence thesis by ZFMISC_1: 87;

        end;

        then Y c= X;

        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 XFAMILY:sch 2( A7, A8);

        hence thesis;

      end;

    end

    theorem :: TOLER_1:30

    ( TolClasses R) c= ( TolClasses T) implies R c= T

    proof

      assume

       A1: ( TolClasses R) c= ( TolClasses T);

      let x,y be object;

      assume [x, y] in R;

      then

      consider Z be 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 :: TOLER_1:31

    for T,R be 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 :: TOLER_1:32

    ( union ( TolClasses T)) = X

    proof

      for x be object holds x in ( union ( TolClasses T)) iff x in X

      proof

        let x be object;

        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 be 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: 2;

    end;

    theorem :: TOLER_1:33

    ( union ( TolSets T)) = X

    proof

      for x be object holds x in ( union ( TolSets T)) iff x in X

      proof

        let x be object;

        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 be 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: 2;

    end;

    theorem :: TOLER_1:34

    (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 be object 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 be object;

        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);

      hence thesis;

    end;

    theorem :: TOLER_1:35

    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;

      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;

      end;

      then

      reconsider Z = N as TolSet of T by Def1;

      for x st not x in Z & x in X holds 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 :: TOLER_1:36

    for x holds for Y be 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 be object st y in Y holds y in ( neighbourhood (x,T))

      proof

        let y be object;

        assume y in Y;

        then [x, y] in T by A1, Def1;

        hence thesis by Th27;

      end;

      hence thesis;

    end;

    theorem :: TOLER_1:37

    ( 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 be object;

        assume [x, y] in R;

        then

        consider Z be 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 be object;

      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 by Def1, A3;

      then Z is TolSet of T by Def1;

      hence thesis by Def3;

    end;

    theorem :: TOLER_1:38

    ( TolClasses T) c= ( TolSets T)

    proof

      let x be object;

      assume x in ( TolClasses T);

      then x is TolSet of T by Def4;

      hence thesis by Def3;

    end;

    theorem :: TOLER_1:39

    (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 be object;

      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 :: TOLER_1:40

    T c= (T * T)

    proof

      let x,y be object;

      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;