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 S₁[ 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 & S₁[x] ) ) from XFAMILY: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 by A1;
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;
then A18: Y c= the Element of Z by A2;
let x be object ; :: 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;
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} ;
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