:: TOLER_1 semantic presentation

begin


registration
cluster Relation-like empty  ->  reflexive irreflexive symmetric antisymmetric asymmetric connected strongly_connected transitive for set ;
coherence
 for b1 being Relation st b1 is empty holds
( b1 is reflexive & b1 is irreflexive & b1 is symmetric & b1 is antisymmetric & b1 is asymmetric & b1 is connected & b1 is strongly_connected & b1 is transitive )
proof
let R be Relation; ::_thesis: ( R is empty implies ( R is reflexive & R is irreflexive & R is symmetric & R is antisymmetric & R is asymmetric & R is connected & R is strongly_connected & R is transitive ) )
assume A1: R is empty ; ::_thesis: ( R is reflexive & R is irreflexive & R is symmetric & R is antisymmetric & R is asymmetric & R is connected & R is strongly_connected & R is transitive )
 for x being set st x in {} holds
[x,x] in {} ;
then  {} is_reflexive_in field {} by RELAT_2:def_1;
hence  R is reflexive by A1, RELAT_2:def_9; ::_thesis: ( R is irreflexive & R is symmetric & R is antisymmetric & R is asymmetric & R is connected & R is strongly_connected & R is transitive )
 {} is_irreflexive_in field {}
proof
let x be set ; :: according to RELAT_2:def_2 ::_thesis: ( not x in field {} or not [x,x] in {} )
assume  x in field {} ; ::_thesis: not [x,x] in {}
thus  not [x,x] in {} ; ::_thesis: verum
end;
hence  R is irreflexive by A1, RELAT_2:def_10; ::_thesis: ( R is symmetric & R is antisymmetric & R is asymmetric & R is connected & R is strongly_connected & R is transitive )
thus  R is symmetric ::_thesis: ( R is antisymmetric & R is asymmetric & R is connected & R is strongly_connected & R is transitive )
proof
let x be set ; :: according to RELAT_2:def_3,RELAT_2:def_11 ::_thesis: for b1 being set holds
( not x in field R or not b1 in field R or not [x,b1] in R or [b1,x] in R )
let y be set ; ::_thesis: ( not x in field R or not y in field R or not [x,y] in R or [y,x] in R )
assume that
 x in field R and
 y in field R and
A2: [x,y] in R ; ::_thesis: [y,x] in R
thus  [y,x] in R by A1, A2; ::_thesis: verum
end;
 {} is_antisymmetric_in field {}
proof
let x be set ; :: according to RELAT_2:def_4 ::_thesis: for b1 being set holds
( not x in field {} or not b1 in field {} or not [x,b1] in {} or not [b1,x] in {} or x = b1 )
let y be set ; ::_thesis: ( not x in field {} or not y in field {} or not [x,y] in {} or not [y,x] in {} or x = y )
assume that
A3: x in field {} and
 y in field {} and
 [x,y] in {} and
 [y,x] in {} ; ::_thesis: x = y
thus  x = y by A3; ::_thesis: verum
end;
hence  R is antisymmetric by A1, RELAT_2:def_12; ::_thesis: ( R is asymmetric & R is connected & R is strongly_connected & R is transitive )
 {} is_asymmetric_in field {}
proof
let x be set ; :: according to RELAT_2:def_5 ::_thesis: for b1 being set holds
( not x in field {} or not b1 in field {} or not [x,b1] in {} or not [b1,x] in {} )
let y be set ; ::_thesis: ( not x in field {} or not y in field {} or not [x,y] in {} or not [y,x] in {} )
assume that
 x in field {} and
 y in field {} and
 [x,y] in {} ; ::_thesis: not [y,x] in {}
thus  not [y,x] in {} ; ::_thesis: verum
end;
hence  R is asymmetric by A1, RELAT_2:def_13; ::_thesis: ( R is connected & R is strongly_connected & R is transitive )
 {} is_connected_in field {}
proof
let x be set ; :: according to RELAT_2:def_6 ::_thesis: for b1 being set holds
( not x in field {} or not b1 in field {} or x = b1 or [x,b1] in {} or [b1,x] in {} )
let y be set ; ::_thesis: ( not x in field {} or not y in field {} or x = y or [x,y] in {} or [y,x] in {} )
assume that
A4: x in field {} and
 y in field {} and
 x <> y ; ::_thesis: ( [x,y] in {} or [y,x] in {} )
thus  ( [x,y] in {} or [y,x] in {} ) by A4; ::_thesis: verum
end;
hence  R is connected by A1, RELAT_2:def_14; ::_thesis: ( R is strongly_connected & R is transitive )
 {} is_strongly_connected_in field {}
proof
let x be set ; :: according to RELAT_2:def_7 ::_thesis: for b1 being set holds
( not x in field {} or not b1 in field {} or [x,b1] in {} or [b1,x] in {} )
let y be set ; ::_thesis: ( not x in field {} or not y in field {} or [x,y] in {} or [y,x] in {} )
assume that
A5: x in field {} and
 y in field {} ; ::_thesis: ( [x,y] in {} or [y,x] in {} )
thus  ( [x,y] in {} or [y,x] in {} ) by A5; ::_thesis: verum
end;
hence  R is strongly_connected by A1, RELAT_2:def_15; ::_thesis: R is transitive
 {} is_transitive_in field {}
proof
let x be set ; :: according to RELAT_2:def_8 ::_thesis: for b1, b2 being set holds
( not x in field {} or not b1 in field {} or not b2 in field {} or not [x,b1] in {} or not [b1,b2] in {} or [x,b2] in {} )
let y, z be set ; ::_thesis: ( not x in field {} or not y in field {} or not z in field {} or not [x,y] in {} or not [y,z] in {} or [x,z] in {} )
assume that
A6: x in field {} and
 y in field {} and
 z in field {} and
 [x,y] in {} and
 [y,z] in {} ; ::_thesis: [x,z] in {}
thus  [x,z] in {} by A6; ::_thesis: verum
end;
hence  R is transitive by A1, RELAT_2:def_16; ::_thesis: verum
end;
end;

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

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

theorem :: TOLER_1:1
for X being set holds rng (Total X) = X
proof
let X be set ; ::_thesis: rng (Total X) = X
 for x being set holds
( x in X iff ex y being set st [y,x] in Total X )
proof
let x be set ; ::_thesis: ( x in X iff ex y being set st [y,x] in Total X )
thus  ( x in X implies ex y being set st [y,x] in Total X ) ::_thesis: ( ex y being set st [y,x] in Total X implies x in X )
proof
assume A1: x in X ; ::_thesis: ex y being set st [y,x] in Total X
take  x ; ::_thesis: [x,x] in Total X
 [x,x] in [:X,X:] by A1, ZFMISC_1:87;
hence  [x,x] in Total X by EQREL_1:def_1; ::_thesis: verum
end;
given y being set  such that A2: [y,x] in Total X ; ::_thesis: x in X
thus  x in X by A2, ZFMISC_1:87; ::_thesis: verum
end;
hence  rng (Total X) = X by XTUPLE_0:def_13; ::_thesis: verum
end;

theorem Th2: :: TOLER_1:2
for X, x, y being set st x in X & y in X holds
[x,y] in Total X
proof
let X, x, y be set ; ::_thesis: ( x in X & y in X implies [x,y] in Total X )
assume  ( x in X & y in X ) ; ::_thesis: [x,y] in Total X
then  [x,y] in [:X,X:] by ZFMISC_1:87;
hence  [x,y] in Total X by EQREL_1:def_1; ::_thesis: verum
end;

theorem :: TOLER_1:3
for X, x, y being set st x in field (Total X) & y in field (Total X) holds
[x,y] in Total X
proof
let X, x, y be set ; ::_thesis: ( x in field (Total X) & y in field (Total X) implies [x,y] in Total X )
assume  ( x in field (Total X) & y in field (Total X) ) ; ::_thesis: [x,y] in Total X
then  ( x in X & y in X ) by ORDERS_1:12;
hence  [x,y] in Total X by Th2; ::_thesis: verum
end;

theorem :: TOLER_1:4
for X being set holds Total X is strongly_connected
proof
let X be set ; ::_thesis: Total X is strongly_connected
let x be set ; :: according to RELAT_2:def_7,RELAT_2:def_15 ::_thesis: for b1 being set holds
( not x in field (Total X) or not b1 in field (Total X) or [x,b1] in Total X or [b1,x] in Total X )
let y be set ; ::_thesis: ( not x in field (Total X) or not y in field (Total X) or [x,y] in Total X or [y,x] in Total X )
assume  ( x in field (Total X) & y in field (Total X) ) ; ::_thesis: ( [x,y] in Total X or [y,x] in Total X )
then  ( x in X & y in X ) by ORDERS_1:12;
then  [x,y] in [:X,X:] by ZFMISC_1:87;
hence  ( [x,y] in Total X or [y,x] in Total X ) by EQREL_1:def_1; ::_thesis: verum
end;

theorem :: TOLER_1:5
for X being set holds Total X is connected
proof
let X be set ; ::_thesis: Total X is connected
let x be set ; :: according to RELAT_2:def_6,RELAT_2:def_14 ::_thesis: for b1 being set holds
( not x in field (Total X) or not b1 in field (Total X) or x = b1 or [x,b1] in Total X or [b1,x] in Total X )
let y be set ; ::_thesis: ( not x in field (Total X) or not y in field (Total X) or x = y or [x,y] in Total X or [y,x] in Total X )
assume that
A1: ( x in field (Total X) & y in field (Total X) ) and
 x <> y ; ::_thesis: ( [x,y] in Total X or [y,x] in Total X )
 ( x in X & y in X ) by A1, ORDERS_1:12;
then  [x,y] in [:X,X:] by ZFMISC_1:87;
hence  ( [x,y] in Total X or [y,x] in Total X ) by EQREL_1:def_1; ::_thesis: verum
end;


theorem :: TOLER_1:6
for X being set
for T being Tolerance of X holds rng T = X
proof
let X be set ; ::_thesis: for T being Tolerance of X holds rng T = X
let T be Tolerance of X; ::_thesis: rng T = X
 for x being set holds
( x in rng T iff x in X )
proof
let x be set ; ::_thesis: ( x in rng T iff x in 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 ; ::_thesis: x in rng T
then  [x,x] in T by A1, RELAT_2:def_1;
hence  x in rng T by XTUPLE_0:def_13; ::_thesis: verum
end;
hence  ( x in rng T iff x in X ) ; ::_thesis: verum
end;
hence  rng T = X by TARSKI:1; ::_thesis: verum
end;

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

theorem :: TOLER_1:8
for X being set
for T being Tolerance of X holds T is_reflexive_in X
proof
let X be set ; ::_thesis: for T being Tolerance of X holds T is_reflexive_in X
let T be Tolerance of X; ::_thesis: T is_reflexive_in X
 field T = X by ORDERS_1:12;
hence  T is_reflexive_in X by RELAT_2:def_9; ::_thesis: verum
end;

theorem :: TOLER_1:9
for X being set
for T being Tolerance of X holds T is_symmetric_in X
proof
let X be set ; ::_thesis: for T being Tolerance of X holds T is_symmetric_in X
let T be Tolerance of X; ::_thesis: T is_symmetric_in X
 field T = X by ORDERS_1:12;
hence  T is_symmetric_in X by RELAT_2:def_11; ::_thesis: verum
end;

theorem Th10: :: TOLER_1:10
for X, Y, Z being set
for R being Relation of X,Y st R is symmetric holds
R |_2 Z is symmetric
proof
let X, Y, Z be set ; ::_thesis: for R being Relation of X,Y st R is symmetric holds
R |_2 Z is symmetric
let R be Relation of X,Y; ::_thesis: ( R is symmetric implies R |_2 Z is symmetric )
assume  R is symmetric ; ::_thesis: R |_2 Z is symmetric
then A1: R is_symmetric_in field R by RELAT_2:def_11;
now__::_thesis:_for_x,_y_being_set_st_x_in_field_(R_|_2_Z)_&_y_in_field_(R_|_2_Z)_&_[x,y]_in_R_|_2_Z_holds_
[y,x]_in_R_|_2_Z
let x, y be set ; ::_thesis: ( x in field (R |_2 Z) & y in field (R |_2 Z) & [x,y] in R |_2 Z implies [y,x] in R |_2 Z )
assume that
A2: ( x in field (R |_2 Z) & y in field (R |_2 Z) ) and
A3: [x,y] in R |_2 Z ; ::_thesis: [y,x] 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; ::_thesis: verum
end;
then  R |_2 Z is_symmetric_in field (R |_2 Z) by RELAT_2:def_3;
hence  R |_2 Z is symmetric by RELAT_2:def_11; ::_thesis: verum
end;

definition
let X be set ;
let T be Tolerance of X;
let Y be Subset of X;
:: original: |_2
redefine funcT |_2 Y ->  Tolerance of Y;
coherence
 T |_2 Y is Tolerance of Y
proof
now__::_thesis:_for_x_being_set_st_x_in_Y_holds_
x_in_dom_(T_|_2_Y)
let x be set ; ::_thesis: ( x in Y implies x in dom (T |_2 Y) )
assume  x in Y ; ::_thesis: x in dom (T |_2 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; ::_thesis: verum
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; ::_thesis: verum
end;
end;

theorem :: TOLER_1:11
for Y, X being set
for T being Tolerance of X st Y c= X holds
T |_2 Y is Tolerance of Y
proof
let Y, X be set ; ::_thesis: for T being Tolerance of X st Y c= X holds
T |_2 Y is Tolerance of Y
let T be Tolerance of X; ::_thesis: ( Y c= X implies T |_2 Y is Tolerance of Y )
assume  Y c= X ; ::_thesis: T |_2 Y is Tolerance of Y
then reconsider Z = Y as Subset of X ;
 T |_2 Z is Tolerance of Z ;
hence  T |_2 Y is Tolerance of Y ; ::_thesis: verum
end;

definition
let X be set ;
let T be Tolerance of X;
mode TolSet of T ->  set  means :Def1: :: TOLER_1:def 1
 for x, y being set st x in it & y in it holds
[x,y] in T;
existence
 ex b1 being set st
for x, y being set st x in b1 & y in b1 holds
[x,y] in T
proof
take  {} ; ::_thesis: for x, y being set st x in {} & y in {} holds
[x,y] in T
let x, y be set ; ::_thesis: ( x in {} & y in {} implies [x,y] in T )
assume that
A1: x in {} and
 y in {} ; ::_thesis: [x,y] in T
thus  [x,y] in T by A1; ::_thesis: verum
end;
end;

:: deftheorem Def1 defines TolSet TOLER_1:def_1_:_
 for X being set
for T being Tolerance of X
for b3 being set holds
( b3 is TolSet of T iff for x, y being set st x in b3 & y in b3 holds
[x,y] in T );

theorem Th12: :: TOLER_1:12
for X being set
for T being Tolerance of X holds {} is TolSet of T
proof
let X be set ; ::_thesis: for T being Tolerance of X holds {} is TolSet of T
let T be Tolerance of X; ::_thesis: {} is TolSet of T
let x be set ; :: according to TOLER_1:def_1 ::_thesis: for y being set st x in {} & y in {} holds
[x,y] in T
let y be set ; ::_thesis: ( x in {} & y in {} implies [x,y] in T )
assume that
A1: x in {} and
 y in {} ; ::_thesis: [x,y] in T
thus  [x,y] in T by A1; ::_thesis: verum
end;

definition
let X be set ;
let T be Tolerance of X;
let IT be TolSet of T;
attrIT is TolClass-like  means :Def2: :: TOLER_1:def 2
 for x being set st not x in IT & x in X holds
ex y being set st
( y in IT & not [x,y] in T );
end;

:: deftheorem Def2 defines TolClass-like TOLER_1:def_2_:_
 for X being set
for T being Tolerance of X
for IT being TolSet of T holds
( IT is TolClass-like iff for x being set st not x in IT & x in X holds
ex y being set st
( y in IT & not [x,y] in T ) );

registration
let X be set ;
let T be Tolerance of X;
cluster TolClass-like for TolSet of T;
existence
 ex b1 being TolSet of T st b1 is TolClass-like
proof
defpred S1[ set ] means X is TolSet of T;
consider TS being set  such that
A1: for x being set holds
( x in TS iff ( x in bool X & S1[x] ) ) from XBOOLE_0:sch_1();
A2: TS c= bool X
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in TS or x in bool X )
assume  x in TS ; ::_thesis: x in bool X
hence  x in bool X by A1; ::_thesis: verum
end;
A3: for Z being set st Z c= TS & Z is c=-linear holds
ex Y being set st
( Y in TS & ( for X1 being set st X1 in Z holds
X1 c= Y ) )
proof
let Z be set ; ::_thesis: ( Z c= TS & Z is c=-linear implies ex Y being set st
( Y in TS & ( for X1 being set st X1 in Z holds
X1 c= Y ) ) )
assume that
A4: Z c= TS and
A5: Z is c=-linear ; ::_thesis: ex Y being set st
( Y in TS & ( for X1 being set st X1 in Z holds
X1 c= Y ) )
 for x, y being set st x in union Z & y in union Z holds
[x,y] in T
proof
let x, y be set ; ::_thesis: ( x in union Z & y in union Z implies [x,y] in T )
assume that
A6: x in union Z and
A7: y in union Z ; ::_thesis: [x,y] in T
consider Zy being set  such that
A8: y in Zy and
A9: Zy in Z by A7, TARSKI:def_4;
reconsider Zy = 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 = 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  [x,y] in T by A10, A8, Def1; ::_thesis: verum
end;
then A12: union Z is TolSet of T by Def1;
take  union Z ; ::_thesis: ( union Z in TS & ( for X1 being set st X1 in Z holds
X1 c= 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; ::_thesis: for X1 being set st X1 in Z holds
X1 c= union Z
let X1 be set ; ::_thesis: ( X1 in Z implies X1 c= union Z )
assume  X1 in Z ; ::_thesis: X1 c= union Z
hence  X1 c= union Z by ZFMISC_1:74; ::_thesis: verum
end;
 ( {} c= X & {} is TolSet of T ) by Th12, XBOOLE_1:2;
then  TS <> {} by A1;
then consider Y being set  such that
A13: Y in TS and
A14: for Z being set st Z in TS & Z <> Y holds
not Y c= Z by A3, ORDERS_1:65;
reconsider Y = Y as TolSet of T by A1, A13;
take  Y ; ::_thesis: Y is TolClass-like
let x be set ; :: according to TOLER_1:def_2 ::_thesis: ( not x in Y & x in X implies ex y being set st
( y in Y & not [x,y] in T ) )
assume that
A15: not x in Y and
A16: x in X ; ::_thesis: ex y being set st
( y in Y & not [x,y] in T )
set Y1 = Y \/ {x};
A17: {x} c= X by A16, ZFMISC_1:31;
assume A18: for y being set st y in Y holds
[x,y] in T ; ::_thesis: contradiction
 for y, z being set st y in Y \/ {x} & z in Y \/ {x} holds
[y,z] in T
proof
let y, z be set ; ::_thesis: ( y in Y \/ {x} & z in Y \/ {x} implies [y,z] in T )
assume that
A19: y in Y \/ {x} and
A20: z in Y \/ {x} ; ::_thesis: [y,z] in T
 ( 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 ; ::_thesis: contradiction
then  not [z,y] in T by EQREL_1:6;
hence  contradiction by A16, A18, A21, A22, A23, Def1, Th7; ::_thesis: verum
end;
then A24: Y \/ {x} is TolSet of T by Def1;
A25: Y \/ {x} <> Y
proof
A26: x in {x} by TARSKI:def_1;
assume  Y \/ {x} = Y ; ::_thesis: contradiction
hence  contradiction by A15, A26, XBOOLE_0:def_3; ::_thesis: verum
end;
 Y in bool X by A1, A13;
then  Y \/ {x} c= X by A17, XBOOLE_1:8;
then  Y \/ {x} in TS by A1, A24;
hence  contradiction by A14, A25, XBOOLE_1:7; ::_thesis: verum
end;
end;

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

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

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

theorem Th15: :: TOLER_1:15
for X being set
for T being Tolerance of X
for x, y being set st [x,y] in T holds
{x,y} is TolSet of T
proof
let X be set ; ::_thesis: for T being Tolerance of X
for x, y being set st [x,y] in T holds
{x,y} is TolSet of T
let T be Tolerance of X; ::_thesis: for x, y being set st [x,y] in T holds
{x,y} is TolSet of T
let x, y be set ; ::_thesis: ( [x,y] in T implies {x,y} is TolSet of T )
assume A1: [x,y] in T ; ::_thesis: {x,y} is TolSet of 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 ; ::_thesis: ( a in {x,y} & b in {x,y} implies [a,b] in T )
assume that
A3: a in {x,y} and
A4: b in {x,y} ; ::_thesis: [a,b] in T
A5: ( b = x or b = y ) by A4, TARSKI:def_2;
 ( a = x or a = y ) by A3, TARSKI:def_2;
hence  [a,b] in T by A1, A2, A5, Th7, EQREL_1:6; ::_thesis: verum
end;
hence  {x,y} is TolSet of T by Def1; ::_thesis: verum
end;

theorem :: TOLER_1:16
for X being set
for T being Tolerance of X
for x being set st x in X holds
{x} is TolSet of T
proof
let X be set ; ::_thesis: for T being Tolerance of X
for x being set st x in X holds
{x} is TolSet of T
let T be Tolerance of X; ::_thesis: for x being set st x in X holds
{x} is TolSet of T
let x be set ; ::_thesis: ( x in X implies {x} is TolSet of T )
assume  x in X ; ::_thesis: {x} is TolSet of T
then  [x,x] in T by Th7;
then  {x,x} is TolSet of T by Th15;
hence  {x} is TolSet of T by ENUMSET1:29; ::_thesis: verum
end;

theorem :: TOLER_1:17
for X being set
for T being Tolerance of X
for Y, Z being set st Y is TolSet of T holds
Y /\ Z is TolSet of T
proof
let X be set ; ::_thesis: for T being Tolerance of X
for Y, Z being set st Y is TolSet of T holds
Y /\ Z is TolSet of T
let T be Tolerance of X; ::_thesis: for Y, Z being set st Y is TolSet of T holds
Y /\ Z is TolSet of T
let Y, Z be set ; ::_thesis: ( Y is TolSet of T implies Y /\ Z is TolSet of T )
assume A1: Y is TolSet of T ; ::_thesis: Y /\ Z is TolSet of T
let x be set ; :: according to TOLER_1:def_1 ::_thesis: for y being set st x in Y /\ Z & y in Y /\ Z holds
[x,y] in T
let y be set ; ::_thesis: ( x in Y /\ Z & y in Y /\ Z implies [x,y] in T )
assume  ( x in Y /\ Z & y in Y /\ Z ) ; ::_thesis: [x,y] in T
then  ( x in Y & y in Y ) by XBOOLE_0:def_4;
hence  [x,y] in T by A1, Def1; ::_thesis: verum
end;

theorem Th18: :: TOLER_1:18
for Y, X being set
for T being Tolerance of X st Y is TolSet of T holds
Y c= X
proof
let Y, X be set ; ::_thesis: for T being Tolerance of X st Y is TolSet of T holds
Y c= X
let T be Tolerance of X; ::_thesis: ( Y is TolSet of T implies Y c= X )
assume A1: Y is TolSet of T ; ::_thesis: Y c= X
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Y or x in X )
assume  x in Y ; ::_thesis: x in X
then  [x,x] in T by A1, Def1;
hence  x in X by Th7; ::_thesis: verum
end;

theorem Th19: :: TOLER_1:19
for X being set
for T being Tolerance of X
for Y being TolSet of T ex Z being TolClass of T st Y c= Z
proof
let X be set ; ::_thesis: for T being Tolerance of X
for Y being TolSet of T ex Z being TolClass of T st Y c= Z
let T be Tolerance of X; ::_thesis: for Y being TolSet of T ex Z being TolClass of T st Y c= Z
let Y be TolSet of T; ::_thesis: ex Z being TolClass of T st Y c= Z
defpred S1[ set ] means ( $1 is TolSet of T & ex Z being set st
( $1 = Z & Y c= Z ) );
consider TS being set  such that
A1: for x being set holds
( x in TS iff ( x in bool X & S1[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 ; ::_thesis: ( x in TS iff ( x in bool X & x is TolSet of T & Y c= x ) )
thus  ( x in TS implies ( x in bool X & x is TolSet of T & Y c= x ) ) ::_thesis: ( x in bool X & x is TolSet of T & Y c= x implies x in TS )
proof
assume A3: x in TS ; ::_thesis: ( x in bool X & x is TolSet of T & Y c= x )
hence  ( x in bool X & x is TolSet of T ) by A1; ::_thesis: Y c= x
 ex Z being set st
( x = Z & Y c= Z ) by A1, A3;
hence  Y c= x ; ::_thesis: verum
end;
thus  ( x in bool X & x is TolSet of T & Y c= x implies x in TS ) by A1; ::_thesis: verum
end;
 Y c= X by Th18;
then A4: TS <> {} by A2;
A5: TS c= bool X
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in TS or x in bool X )
assume  x in TS ; ::_thesis: x in bool X
hence  x in bool X by A1; ::_thesis: verum
end;
 for Z being set st Z c= TS & Z is c=-linear holds
ex Y being set st
( Y in TS & ( for X1 being set st X1 in Z holds
X1 c= Y ) )
proof
let Z be set ; ::_thesis: ( Z c= TS & Z is c=-linear implies ex Y being set st
( Y in TS & ( for X1 being set st X1 in Z holds
X1 c= Y ) ) )
assume that
A6: Z c= TS and
A7: Z is c=-linear ; ::_thesis: ex Y being set st
( Y in TS & ( for X1 being set st X1 in Z holds
X1 c= Y ) )
A8: for x, y being set st x in union Z & y in union Z holds
[x,y] in T
proof
let x, y be set ; ::_thesis: ( x in union Z & y in union Z implies [x,y] in T )
assume that
A9: x in union Z and
A10: y in union Z ; ::_thesis: [x,y] in T
consider Zy being set  such that
A11: y in Zy and
A12: Zy in Z by A10, TARSKI:def_4;
reconsider Zy = 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 = 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  [x,y] in T by A13, A11, Def1; ::_thesis: verum
end;
A15: ( Z <> {} implies ex Y being set st
( Y in TS & ( for X1 being set st X1 in Z holds
X1 c= Y ) ) )
proof
assume A16: Z <> {} ; ::_thesis: ex Y being set st
( Y in TS & ( for X1 being set st X1 in Z holds
X1 c= Y ) )
A17: Y c= union Z
proof
set y = the Element of Z;
 the Element of Z in TS by A6, A16, TARSKI:def_3;
then A18: Y c= the Element of Z by A2;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Y or x in union Z )
assume  x in Y ; ::_thesis: x in union Z
hence  x in union Z by A16, A18, TARSKI:def_4; ::_thesis: verum
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 ; ::_thesis: ( union Z in TS & ( for X1 being set st X1 in Z holds
X1 c= union Z ) )
 union Z is TolSet of T by A8, Def1;
hence  union Z in TS by A2, A19, A17; ::_thesis: for X1 being set st X1 in Z holds
X1 c= union Z
let X1 be set ; ::_thesis: ( X1 in Z implies X1 c= union Z )
assume  X1 in Z ; ::_thesis: X1 c= union Z
hence  X1 c= union Z by ZFMISC_1:74; ::_thesis: verum
end;
 ( Z = {} implies ex Y being set st
( Y in TS & ( for X1 being set st X1 in Z holds
X1 c= Y ) ) )
proof
set Y = the Element of TS;
assume A20: Z = {} ; ::_thesis: ex Y being set st
( Y in TS & ( for X1 being set st X1 in Z holds
X1 c= Y ) )
take  the Element of TS ; ::_thesis: ( the Element of TS in TS & ( for X1 being set st X1 in Z holds
X1 c= the Element of TS ) )
thus  the Element of TS in TS by A4; ::_thesis: for X1 being set st X1 in Z holds
X1 c= the Element of TS
let X1 be set ; ::_thesis: ( X1 in Z implies X1 c= the Element of TS )
assume  X1 in Z ; ::_thesis: X1 c= the Element of TS
hence  X1 c= the Element of TS by A20; ::_thesis: verum
end;
hence  ex Y being set st
( Y in TS & ( for X1 being set st X1 in Z holds
X1 c= Y ) ) by A15; ::_thesis: verum
end;
then consider Z1 being set  such that
A21: Z1 in TS and
A22: for Z being set st Z in TS & Z <> Z1 holds
not Z1 c= Z by A4, ORDERS_1:65;
reconsider Z1 = Z1 as TolSet of T by A1, A21;
 Z1 is TolClass of T
proof
assume  Z1 is not TolClass of T ; ::_thesis: contradiction
then consider x being set  such that
A23: not x in Z1 and
A24: x in X and
A25: for y being set 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 being set st y in Z1 \/ {x} & z in Z1 \/ {x} holds
[y,z] in T
proof
let y, z be set ; ::_thesis: ( y in Z1 \/ {x} & z in Z1 \/ {x} implies [y,z] in T )
assume that
A27: y in Z1 \/ {x} and
A28: z in Z1 \/ {x} ; ::_thesis: [y,z] in T
 ( 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 ; ::_thesis: contradiction
then  not [z,y] in T by EQREL_1:6;
hence  contradiction by A24, A25, A29, A30, A31, Def1, Th7; ::_thesis: verum
end;
then A32: Z1 \/ {x} is TolSet of T by Def1;
 ( Y c= Z1 & Z1 c= Z1 \/ {x} ) by A2, A21, XBOOLE_1:7;
then A33: Y c= Z1 \/ {x} by XBOOLE_1:1;
A34: Z1 \/ {x} <> Z1
proof
A35: x in {x} by TARSKI:def_1;
assume  Z1 \/ {x} = Z1 ; ::_thesis: contradiction
hence  contradiction by A23, A35, XBOOLE_0:def_3; ::_thesis: verum
end;
 Z1 in bool X by A1, A21;
then  Z1 \/ {x} c= X by A26, XBOOLE_1:8;
then  Z1 \/ {x} in TS by A2, A32, A33;
hence  contradiction by A22, A34, XBOOLE_1:7; ::_thesis: verum
end;
then reconsider Z1 = Z1 as TolClass of T ;
take  Z1 ; ::_thesis: Y c= Z1
thus  Y c= Z1 by A2, A21; ::_thesis: verum
end;

theorem Th20: :: TOLER_1:20
for X being set
for T being Tolerance of X
for x, y being set st [x,y] in T holds
ex Z being TolClass of T st
( x in Z & y in Z )
proof
let X be set ; ::_thesis: for T being Tolerance of X
for x, y being set st [x,y] in T holds
ex Z being TolClass of T st
( x in Z & y in Z )
let T be Tolerance of X; ::_thesis: for x, y being set st [x,y] in T holds
ex Z being TolClass of T st
( x in Z & y in Z )
let x, y be set ; ::_thesis: ( [x,y] in T implies ex Z being TolClass of T st
( x in Z & y in Z ) )
assume A1: [x,y] in T ; ::_thesis: ex Z being TolClass of T st
( x in Z & y in Z )
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 ; ::_thesis: ( a in {x,y} & b in {x,y} implies [a,b] in T )
assume that
A3: a in {x,y} and
A4: b in {x,y} ; ::_thesis: [a,b] in T
A5: ( b = x or b = y ) by A4, TARSKI:def_2;
 ( a = x or a = y ) by A3, TARSKI:def_2;
hence  [a,b] in T by A1, A2, A5, Th7, EQREL_1:6; ::_thesis: verum
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 ; ::_thesis: ( x in Z & y in Z )
 x in {x,y} by TARSKI:def_2;
hence  x in Z by A6; ::_thesis: y in Z
 y in {x,y} by TARSKI:def_2;
hence  y in Z by A6; ::_thesis: verum
end;

theorem Th21: :: TOLER_1:21
for X being set
for T being Tolerance of X
for x being set st x in X holds
ex Z being TolClass of T st x in Z
proof
let X be set ; ::_thesis: for T being Tolerance of X
for x being set st x in X holds
ex Z being TolClass of T st x in Z
let T be Tolerance of X; ::_thesis: for x being set st x in X holds
ex Z being TolClass of T st x in Z
let x be set ; ::_thesis: ( x in X implies ex Z being TolClass of T st x in Z )
assume  x in X ; ::_thesis: ex Z being TolClass of T st x in Z
then  [x,x] in T by Th7;
then  ex Z being TolClass of T st
( x in Z & x in Z ) by Th20;
hence  ex Z being TolClass of T st x in Z ; ::_thesis: verum
end;

theorem :: TOLER_1:22
for X being set
for T being Tolerance of X holds T c= Total X
proof
let X be set ; ::_thesis: for T being Tolerance of X holds T c= Total X
let T be Tolerance of X; ::_thesis: T c= Total X
let x be set ; :: according to RELAT_1:def_3 ::_thesis: for b1 being set holds
( not [x,b1] in T or [x,b1] in Total X )
let y be set ; ::_thesis: ( not [x,y] in T or [x,y] in Total X )
assume  [x,y] in T ; ::_thesis: [x,y] in Total X
then  [x,y] in [:X,X:] ;
hence  [x,y] in Total X by EQREL_1:def_1; ::_thesis: verum
end;

theorem :: TOLER_1:23
for X being set
for T being Tolerance of X holds id X c= T
proof
let X be set ; ::_thesis: for T being Tolerance of X holds id X c= T
let T be Tolerance of X; ::_thesis: id X c= T
let x be set ; :: according to RELAT_1:def_3 ::_thesis: for b1 being set holds
( not [x,b1] in id X or [x,b1] in T )
let y be set ; ::_thesis: ( not [x,y] in id X or [x,y] in T )
assume  [x,y] in id X ; ::_thesis: [x,y] in T
then  ( x in X & x = y ) by RELAT_1:def_10;
hence  [x,y] in T by Th7; ::_thesis: verum
end;

scheme :: TOLER_1:sch 1
ToleranceEx{ F1() ->  set , P1[ set , set ] } :
 ex T being Tolerance of F1() st
for x, y being set st x in F1() & y in F1() holds
( [x,y] in T iff P1[x,y] )
provided
A1: for x being set st x in F1() holds
P1[x,x] and
A2: for x, y being set st x in F1() & y in F1() & P1[x,y] holds
P1[y,x]
proof
defpred S1[ set ] means  ex y, z being set st
( $1 = [y,z] & P1[y,z] );
consider T being set  such that
A3: for x being set holds
( x in T iff ( x in [:F1(),F1():] & S1[x] ) ) from XBOOLE_0:sch_1();
 for x being set st x in T holds
x in [:F1(),F1():] by A3;
then reconsider T = T as Relation of F1(),F1() by TARSKI:def_3;
A4: field T c= F1() \/ F1() by RELSET_1:8;
 for x being set st x in field T holds
[x,x] in T
proof
let x be set ; ::_thesis: ( x in field T implies [x,x] in T )
assume  x in field T ; ::_thesis: [x,x] in T
then  ( [x,x] in [:F1(),F1():] & P1[x,x] ) by A1, A4, ZFMISC_1:87;
hence  [x,x] in T by A3; ::_thesis: verum
end;
then A5: T is_reflexive_in field T by RELAT_2:def_1;
 for x, y being set st x in field T & y in field T & [x,y] in T holds
[y,x] in T
proof
let x, y be set ; ::_thesis: ( x in field T & y in field T & [x,y] in T implies [y,x] in T )
assume that
A6: ( x in field T & y in field T ) and
A7: [x,y] in T ; ::_thesis: [y,x] in T
 ( x in F1() & y in F1() & P1[x,y] )
proof
thus  ( x in F1() & y in F1() ) by A4, A6; ::_thesis: P1[x,y]
consider a, b being set  such that
A8: [x,y] = [a,b] and
A9: P1[a,b] by A3, A7;
 x = a by A8, XTUPLE_0:1;
hence  P1[x,y] by A8, A9, XTUPLE_0:1; ::_thesis: verum
end;
then  ( [y,x] in [:F1(),F1():] & P1[y,x] ) by A2, ZFMISC_1:87;
hence  [y,x] in T by A3; ::_thesis: verum
end;
then A10: T is_symmetric_in field T by RELAT_2:def_3;
 for x being set st x in F1() holds
x in dom T
proof
let x be set ; ::_thesis: ( x in F1() implies x in dom T )
assume  x in F1() ; ::_thesis: x in dom T
then  ( [x,x] in [:F1(),F1():] & P1[x,x] ) by A1, ZFMISC_1:87;
then  [x,x] in T by A3;
hence  x in dom T by XTUPLE_0:def_12; ::_thesis: verum
end;
then  F1() c= dom T by TARSKI:def_3;
then  dom T = F1() by XBOOLE_0:def_10;
then reconsider T = T as Tolerance of F1() by A5, A10, PARTFUN1:def_2, RELAT_2:def_9, RELAT_2:def_11;
take  T ; ::_thesis: for x, y being set st x in F1() & y in F1() holds
( [x,y] in T iff P1[x,y] )
let x, y be set ; ::_thesis: ( x in F1() & y in F1() implies ( [x,y] in T iff P1[x,y] ) )
assume A11: ( x in F1() & y in F1() ) ; ::_thesis: ( [x,y] in T iff P1[x,y] )
thus  ( [x,y] in T implies P1[x,y] ) ::_thesis: ( P1[x,y] implies [x,y] in T )
proof
assume  [x,y] in T ; ::_thesis: P1[x,y]
then consider a, b being set  such that
A12: [x,y] = [a,b] and
A13: P1[a,b] by A3;
 x = a by A12, XTUPLE_0:1;
hence  P1[x,y] by A12, A13, XTUPLE_0:1; ::_thesis: verum
end;
assume A14: P1[x,y] ; ::_thesis: [x,y] in T
 [x,y] in [:F1(),F1():] by A11, ZFMISC_1:87;
hence  [x,y] in T by A3, A14; ::_thesis: verum
end;

theorem :: TOLER_1:24
for Y being set ex T being Tolerance of (union Y) st
for Z being set st Z in Y holds
Z is TolSet of T
proof
let Y be set ; ::_thesis: ex T being Tolerance of (union Y) st
for Z being set st Z in Y holds
Z is TolSet of T
defpred S1[ set , set ] means  ex Z being set st
( Z in Y & $1 in Z & $2 in Z );
A1: for x being set st x in union Y holds
S1[x,x]
proof
let x be set ; ::_thesis: ( x in union Y implies S1[x,x] )
assume  x in union Y ; ::_thesis: S1[x,x]
then  ex Z being set st
( x in Z & Z in Y ) by TARSKI:def_4;
hence  S1[x,x] ; ::_thesis: verum
end;
A2: for x, y being set st x in union Y & y in union Y & S1[x,y] holds
S1[y,x] ;
consider T being Tolerance of (union Y) such that
A3: for x, y being set st x in union Y & y in union Y holds
( [x,y] in T iff S1[x,y] ) from TOLER_1:sch_1(A1, A2);
take  T ; ::_thesis: for Z being set st Z in Y holds
Z is TolSet of T
let Z be set ; ::_thesis: ( Z in Y implies Z is TolSet of T )
assume A4: Z in Y ; ::_thesis: Z is TolSet of T
 for x, y being set st x in Z & y in Z holds
[x,y] in T
proof
let x, y be set ; ::_thesis: ( x in Z & y in Z implies [x,y] in T )
assume A5: ( x in Z & y in Z ) ; ::_thesis: [x,y] in T
then  ( x in union Y & y in union Y ) by A4, TARSKI:def_4;
hence  [x,y] in T by A3, A4, A5; ::_thesis: verum
end;
hence  Z is TolSet of T by Def1; ::_thesis: verum
end;

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

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

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

theorem Th27: :: TOLER_1:27
for X, x being set
for T being Tolerance of X
for y being set holds
( y in neighbourhood (,) iff [x,y] in T )
proof
let X, x be set ; ::_thesis: for T being Tolerance of X
for y being set holds
( y in neighbourhood (,) iff [x,y] in T )
let T be Tolerance of X; ::_thesis: for y being set holds
( y in neighbourhood (,) iff [x,y] in T )
let y be set ; ::_thesis: ( y in neighbourhood (,) iff [x,y] in T )
hereby  ::_thesis: ( [x,y] in T implies y in neighbourhood (,) )
assume  y in neighbourhood (,) ; ::_thesis: [x,y] in T
then  [y,x] in T by EQREL_1:19;
hence  [x,y] in T by EQREL_1:6; ::_thesis: verum
end;
assume  [x,y] in T ; ::_thesis: y in neighbourhood (,)
then  [y,x] in T by EQREL_1:6;
hence  y in neighbourhood (,) by EQREL_1:19; ::_thesis: verum
end;

theorem :: TOLER_1:28
for X, x being set
for T being Tolerance of X
for Y being set st ( for Z being set holds
( Z in Y iff ( x in Z & Z is TolClass of T ) ) ) holds
neighbourhood (,) = union Y
proof
let X, x be set ; ::_thesis: for T being Tolerance of X
for Y being set st ( for Z being set holds
( Z in Y iff ( x in Z & Z is TolClass of T ) ) ) holds
neighbourhood (,) = union Y
let T be Tolerance of X; ::_thesis: for Y being set st ( for Z being set holds
( Z in Y iff ( x in Z & Z is TolClass of T ) ) ) holds
neighbourhood (,) = union Y
let Y be set ; ::_thesis: ( ( for Z being set holds
( Z in Y iff ( x in Z & Z is TolClass of T ) ) ) implies neighbourhood (,) = union Y )
assume A1: for Z being set holds
( Z in Y iff ( x in Z & Z is TolClass of T ) ) ; ::_thesis: neighbourhood (,) = union Y
 for y being set holds
( y in neighbourhood (,) iff y in union Y )
proof
let y be set ; ::_thesis: ( y in neighbourhood (,) iff y in union Y )
thus  ( y in neighbourhood (,) implies y in union Y ) ::_thesis: ( y in union Y implies y in neighbourhood (,) )
proof
assume  y in neighbourhood (,) ; ::_thesis: y in union Y
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  y in union Y by A3, TARSKI:def_4; ::_thesis: verum
end;
assume  y in union Y ; ::_thesis: y in neighbourhood (,)
then consider Z being set  such that
A4: y in Z and
A5: Z in Y by TARSKI:def_4;
reconsider Z = Z as TolClass of T by A1, A5;
 x in Z by A1, A5;
then  [x,y] in T by A4, Def1;
hence  y in neighbourhood (,) by Th27; ::_thesis: verum
end;
hence  neighbourhood (,) = union Y by TARSKI:1; ::_thesis: verum
end;

theorem :: TOLER_1:29
for X, x being set
for T being Tolerance of X
for Y being set st ( for Z being set holds
( Z in Y iff ( x in Z & Z is TolSet of T ) ) ) holds
neighbourhood (,) = union Y
proof
let X, x be set ; ::_thesis: for T being Tolerance of X
for Y being set st ( for Z being set holds
( Z in Y iff ( x in Z & Z is TolSet of T ) ) ) holds
neighbourhood (,) = union Y
let T be Tolerance of X; ::_thesis: for Y being set st ( for Z being set holds
( Z in Y iff ( x in Z & Z is TolSet of T ) ) ) holds
neighbourhood (,) = union Y
let Y be set ; ::_thesis: ( ( for Z being set holds
( Z in Y iff ( x in Z & Z is TolSet of T ) ) ) implies neighbourhood (,) = union Y )
assume A1: for Z being set holds
( Z in Y iff ( x in Z & Z is TolSet of T ) ) ; ::_thesis: neighbourhood (,) = union Y
 for y being set holds
( y in neighbourhood (,) iff y in union Y )
proof
let y be set ; ::_thesis: ( y in neighbourhood (,) iff y in union Y )
thus  ( y in neighbourhood (,) implies y in union Y ) ::_thesis: ( y in union Y implies y in neighbourhood (,) )
proof
assume  y in neighbourhood (,) ; ::_thesis: y in union Y
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  y in union Y by A3, TARSKI:def_4; ::_thesis: verum
end;
assume  y in union Y ; ::_thesis: y in neighbourhood (,)
then consider Z being set  such that
A4: y in Z and
A5: Z in Y by TARSKI:def_4;
reconsider Z = Z as TolSet of T by A1, A5;
 x in Z by A1, A5;
then  [x,y] in T by A4, Def1;
hence  y in neighbourhood (,) by Th27; ::_thesis: verum
end;
hence  neighbourhood (,) = union Y by TARSKI:1; ::_thesis: verum
end;

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

:: deftheorem Def3 defines TolSets TOLER_1:def_3_:_
 for X being set
for T being Tolerance of X
for b3 being set holds
( b3 = TolSets T iff for Y being set holds
( Y in b3 iff Y is TolSet of T ) );

:: deftheorem Def4 defines TolClasses TOLER_1:def_4_:_
 for X being set
for T being Tolerance of X
for b3 being set holds
( b3 = TolClasses T iff for Y being set holds
( Y in b3 iff Y is TolClass of T ) );

theorem :: TOLER_1:30
for X being set
for R, T being Tolerance of X st TolClasses R c= TolClasses T holds
R c= T
proof
let X be set ; ::_thesis: for R, T being Tolerance of X st TolClasses R c= TolClasses T holds
R c= T
let R, T be Tolerance of X; ::_thesis: ( TolClasses R c= TolClasses T implies R c= T )
assume A1: TolClasses R c= TolClasses T ; ::_thesis: R c= T
let x be set ; :: according to RELAT_1:def_3 ::_thesis: for b1 being set holds
( not [x,b1] in R or [x,b1] in T )
let y be set ; ::_thesis: ( not [x,y] in R or [x,y] in T )
assume  [x,y] in R ; ::_thesis: [x,y] in T
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  [x,y] in T by A2, Def1; ::_thesis: verum
end;

theorem :: TOLER_1:31
for X being set
for T, R being Tolerance of X st TolClasses T = TolClasses R holds
T = R
proof
let X be set ; ::_thesis: for T, R being Tolerance of X st TolClasses T = TolClasses R holds
T = R
let T, R be Tolerance of X; ::_thesis: ( TolClasses T = TolClasses R implies T = R )
assume A1: TolClasses T = TolClasses R ; ::_thesis: T = R
 for Z being set holds
( Z is TolClass of T iff Z is TolClass of R )
proof
let Z be set ; ::_thesis: ( Z is TolClass of T iff Z is TolClass of R )
 ( Z is TolClass of T iff Z in TolClasses R ) by A1, Def4;
hence  ( Z is TolClass of T iff Z is TolClass of R ) by Def4; ::_thesis: verum
end;
hence  T = R by Th26; ::_thesis: verum
end;

theorem :: TOLER_1:32
for X being set
for T being Tolerance of X holds union (TolClasses T) = X
proof
let X be set ; ::_thesis: for T being Tolerance of X holds union (TolClasses T) = X
let T be Tolerance of X; ::_thesis: union (TolClasses T) = X
 for x being set holds
( x in union (TolClasses T) iff x in X )
proof
let x be set ; ::_thesis: ( x in union (TolClasses T) iff x in X )
thus  ( x in union (TolClasses T) implies x in X ) ::_thesis: ( x in X implies x in union (TolClasses T) )
proof
assume  x in union (TolClasses T) ; ::_thesis: x in X
then consider Z being set  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  x in X by A1; ::_thesis: verum
end;
assume  x in X ; ::_thesis: x in union (TolClasses T)
then consider Z being TolClass of T such that
A3: x in Z by Th21;
 Z in TolClasses T by Def4;
hence  x in union (TolClasses T) by A3, TARSKI:def_4; ::_thesis: verum
end;
hence  union (TolClasses T) = X by TARSKI:1; ::_thesis: verum
end;

theorem :: TOLER_1:33
for X being set
for T being Tolerance of X holds union (TolSets T) = X
proof
let X be set ; ::_thesis: for T being Tolerance of X holds union (TolSets T) = X
let T be Tolerance of X; ::_thesis: union (TolSets T) = X
 for x being set holds
( x in union (TolSets T) iff x in X )
proof
let x be set ; ::_thesis: ( x in union (TolSets T) iff x in X )
thus  ( x in union (TolSets T) implies x in X ) ::_thesis: ( x in X implies x in union (TolSets T) )
proof
assume  x in union (TolSets T) ; ::_thesis: x in X
then consider Z being set  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  x in X by A1; ::_thesis: verum
end;
assume  x in X ; ::_thesis: x in union (TolSets T)
then consider Z being TolClass of T such that
A3: x in Z by Th21;
 Z in TolSets T by Def3;
hence  x in union (TolSets T) by A3, TARSKI:def_4; ::_thesis: verum
end;
hence  union (TolSets T) = X by TARSKI:1; ::_thesis: verum
end;

theorem :: TOLER_1:34
for X being set
for T being Tolerance of X st ( for x being set st x in X holds
neighbourhood (,) is TolSet of T ) holds
T is transitive
proof
let X be set ; ::_thesis: for T being Tolerance of X st ( for x being set st x in X holds
neighbourhood (,) is TolSet of T ) holds
T is transitive
let T be Tolerance of X; ::_thesis: ( ( for x being set st x in X holds
neighbourhood (,) is TolSet of T ) implies T is transitive )
assume A1: for x being set st x in X holds
neighbourhood (,) is TolSet of T ; ::_thesis: T is transitive
A2: field T = X by ORDERS_1:12;
 for x, y, z being set 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 set ; ::_thesis: ( x in field T & y in field T & z in field T & [x,y] in T & [y,z] in T implies [x,z] in T )
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 ; ::_thesis: [x,z] in T
reconsider N = neighbourhood (,) 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  [x,z] in T by A6, Def1; ::_thesis: verum
end;
then  T is_transitive_in field T by RELAT_2:def_8;
hence  T is transitive by RELAT_2:def_16; ::_thesis: verum
end;

theorem :: TOLER_1:35
for X being set
for T being Tolerance of X st T is transitive holds
for x being set st x in X holds
neighbourhood (,) is TolClass of T
proof
let X be set ; ::_thesis: for T being Tolerance of X st T is transitive holds
for x being set st x in X holds
neighbourhood (,) is TolClass of T
let T be Tolerance of X; ::_thesis: ( T is transitive implies for x being set st x in X holds
neighbourhood (,) is TolClass of T )
assume A1: T is transitive ; ::_thesis: for x being set st x in X holds
neighbourhood (,) is TolClass of T
let x be set ; ::_thesis: ( x in X implies neighbourhood (,) is TolClass of T )
assume A2: x in X ; ::_thesis: neighbourhood (,) is TolClass of T
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 being set st y in Class (T,x) & z in Class (T,x) holds
[y,z] in T
proof
let y, z be set ; ::_thesis: ( y in Class (T,x) & z in Class (T,x) implies [y,z] in T )
assume that
A4: y in Class (T,x) and
A5: z in Class (T,x) ; ::_thesis: [y,z] in T
 [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  [y,z] in T by A3, A2, A4, A5, A6, RELAT_2:def_8; ::_thesis: verum
end;
then reconsider Z = Class (T,x) as TolSet of T by Def1;
 for x being set st not x in Z & x in X holds
ex y being set st
( y in Z & not [x,y] in T )
proof
let y be set ; ::_thesis: ( not y in Z & y in X implies ex y being set st
( y in Z & not [y,y] in T ) )
assume that
A7: not y in Z and
 y in X ; ::_thesis: ex y being set st
( y in Z & not [y,y] in T )
A8: x in Z by A2, EQREL_1:20;
assume  for z being set st z in Z holds
[y,z] in T ; ::_thesis: contradiction
then  [y,x] in T by A8;
then  [x,y] in T by EQREL_1:6;
hence  contradiction by A7, Th27; ::_thesis: verum
end;
hence  neighbourhood (,) is TolClass of T by Def2; ::_thesis: verum
end;

theorem :: TOLER_1:36
for X being set
for T being Tolerance of X
for x being set
for Y being TolClass of T st x in Y holds
Y c= neighbourhood (,)
proof
let X be set ; ::_thesis: for T being Tolerance of X
for x being set
for Y being TolClass of T st x in Y holds
Y c= neighbourhood (,)
let T be Tolerance of X; ::_thesis: for x being set
for Y being TolClass of T st x in Y holds
Y c= neighbourhood (,)
let x be set ; ::_thesis: for Y being TolClass of T st x in Y holds
Y c= neighbourhood (,)
let Y be TolClass of T; ::_thesis: ( x in Y implies Y c= neighbourhood (,) )
assume A1: x in Y ; ::_thesis: Y c= neighbourhood (,)
 for y being set st y in Y holds
y in neighbourhood (,)
proof
let y be set ; ::_thesis: ( y in Y implies y in neighbourhood (,) )
assume  y in Y ; ::_thesis: y in neighbourhood (,)
then  [x,y] in T by A1, Def1;
hence  y in neighbourhood (,) by Th27; ::_thesis: verum
end;
hence  Y c= neighbourhood (,) by TARSKI:def_3; ::_thesis: verum
end;

theorem :: TOLER_1:37
for X being set
for R, T being Tolerance of X holds
( TolSets R c= TolSets T iff R c= T )
proof
let X be set ; ::_thesis: for R, T being Tolerance of X holds
( TolSets R c= TolSets T iff R c= T )
let R, T be Tolerance of X; ::_thesis: ( TolSets R c= TolSets T iff R c= T )
thus  ( TolSets R c= TolSets T implies R c= T ) ::_thesis: ( R c= T implies TolSets R c= TolSets T )
proof
assume A1: TolSets R c= TolSets T ; ::_thesis: R c= T
let x be set ; :: according to RELAT_1:def_3 ::_thesis: for b1 being set holds
( not [x,b1] in R or [x,b1] in T )
let y be set ; ::_thesis: ( not [x,y] in R or [x,y] in T )
assume  [x,y] in R ; ::_thesis: [x,y] in T
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  [x,y] in T by A2, Def1; ::_thesis: verum
end;
assume A3: R c= T ; ::_thesis: TolSets R c= TolSets T
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in TolSets R or x in TolSets T )
assume  x in TolSets R ; ::_thesis: x in TolSets T
then reconsider Z = x as TolSet of R by Def3;
 for x, y being set st x in Z & y in Z holds
[x,y] in T
proof
let x, y be set ; ::_thesis: ( x in Z & y in Z implies [x,y] in T )
assume  ( x in Z & y in Z ) ; ::_thesis: [x,y] in T
then  [x,y] in R by Def1;
hence  [x,y] in T by A3; ::_thesis: verum
end;
then  Z is TolSet of T by Def1;
hence  x in TolSets T by Def3; ::_thesis: verum
end;

theorem :: TOLER_1:38
for X being set
for T being Tolerance of X holds TolClasses T c= TolSets T
proof
let X be set ; ::_thesis: for T being Tolerance of X holds TolClasses T c= TolSets T
let T be Tolerance of X; ::_thesis: TolClasses T c= TolSets T
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in TolClasses T or x in TolSets T )
assume  x in TolClasses T ; ::_thesis: x in TolSets T
then  x is TolSet of T by Def4;
hence  x in TolSets T by Def3; ::_thesis: verum
end;

theorem :: TOLER_1:39
for X being set
for R, T being Tolerance of X st ( for x being set st x in X holds
neighbourhood (,) c= neighbourhood (,) ) holds
R c= T
proof
let X be set ; ::_thesis: for R, T being Tolerance of X st ( for x being set st x in X holds
neighbourhood (,) c= neighbourhood (,) ) holds
R c= T
let R, T be Tolerance of X; ::_thesis: ( ( for x being set st x in X holds
neighbourhood (,) c= neighbourhood (,) ) implies R c= T )
assume A1: for x being set st x in X holds
neighbourhood (,) c= neighbourhood (,) ; ::_thesis: R c= T
let x be set ; :: according to RELAT_1:def_3 ::_thesis: for b1 being set holds
( not [x,b1] in R or [x,b1] in T )
let y be set ; ::_thesis: ( not [x,y] in R or [x,y] in T )
assume A2: [x,y] in R ; ::_thesis: [x,y] in T
then  x in X by ZFMISC_1:87;
then A3: neighbourhood (,) c= neighbourhood (,) by A1;
 y in neighbourhood (,) by A2, Th27;
hence  [x,y] in T by A3, Th27; ::_thesis: verum
end;

theorem :: TOLER_1:40
for X being set
for T being Tolerance of X holds T c= T * T
proof
let X be set ; ::_thesis: for T being Tolerance of X holds T c= T * T
let T be Tolerance of X; ::_thesis: T c= T * T
let x be set ; :: according to RELAT_1:def_3 ::_thesis: for b1 being set holds
( not [x,b1] in T or [x,b1] in T * T )
let y be set ; ::_thesis: ( not [x,y] in T or [x,y] in T * T )
assume A1: [x,y] in T ; ::_thesis: [x,y] in T * T
then  y in X by ZFMISC_1:87;
then  [y,y] in T by Th7;
hence  [x,y] in T * T by A1, RELAT_1:def_8; ::_thesis: verum
end;