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

A4: TS <> {}

proof

Y c= X by Th43;
hence TS <> {} by A2; :: thesis: verum

end;

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 A6: ( Z c= TS & 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 ) )
A7: 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 A8: ( x in union Z & y in union Z ) ; :: thesis: [x,y] in T
then consider Zx being set such that
A9: ( x in Zx & Zx in Z ) by TARSKI:def 4;
consider Zy being set such that
A10: ( y in Zy & Zy in Z ) by A8, TARSKI:def 4;
reconsider Zx = Zx as TolSet of T by A1, A6, A9;
reconsider Zy = Zy as TolSet of T by A1, A6, A10;
Zx,Zy are_c=-comparable by A6, A9, A10, ORDINAL1:def 9;
then ( Zx c= Zy or Zy c= Zx ) by XBOOLE_0:def 9;
hence [x,y] in T by A9, A10, Def3; :: thesis: verum

end;

A11: ( Z = {} implies ex Y being set st
( Y in TS & ( for X1 being set st X1 in Z holds
X1 c= Y ) ) )

proof

assume A12: Z = {} ; :: thesis: ex Y being set st
( Y in TS & ( for X1 being set st X1 in Z holds
X1 c= Y ) )
consider Y being Element of TS;
take Y ; :: thesis: ( Y in TS & ( for X1 being set st X1 in Z holds
X1 c= Y ) )
thus Y in TS by A4; :: thesis: for X1 being set st X1 in Z holds
X1 c= Y
let X1 be set ; :: thesis: ( X1 in Z implies X1 c= Y )
assume X1 in Z ; :: thesis: X1 c= Y
hence X1 c= Y by A12; :: 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

assume A13: Z <> {} ; :: thesis: ex Y being set st
( Y in TS & ( for X1 being set st X1 in Z holds
X1 c= Y ) )
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 A5, A6, XBOOLE_1:1;
then union Z c= union (bool X) by ZFMISC_1:95;
then A14: union Z c= X by ZFMISC_1:99;
A15: union Z is TolSet of T by A7, Def3;
Y c= union Z

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Y or x in union Z )
assume A16: x in Y ; :: thesis: x in union Z
consider y being Element of Z;
y in TS by A6, A13, TARSKI:def 3;
then Y c= y by A2;
hence x in union Z by A13, A16, TARSKI:def 4; :: thesis: verum

end;

hence union Z in TS by A2, A14, A15; :: 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:92; :: 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 A11; :: thesis: verum

end;

then consider Z1 being set such that
A17: ( Z1 in TS & ( for Z being set st Z in TS & Z <> Z1 holds
not Z1 c= Z ) ) by A4, ORDERS_1:175;
reconsider Z1 = Z1 as TolSet of T by A1, A17;
Z1 is TolClass of T

proof

assume Z1 is not TolClass of T ; :: thesis: contradiction
then consider x being set such that
A18: ( not x in Z1 & x in X & ( for y being set st y in Z1 holds
[x,y] in T ) ) by Def4;
set Y1 = Z1 \/ {x};
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 ( y in Z1 \/ {x} & z in Z1 \/ {x} ) ; :: thesis: [y,z] in T
then ( ( y in Z1 or y in {x} ) & ( z in Z1 or z in {x} ) ) by XBOOLE_0:def 3;
then A19: ( ( y in Z1 or y = x ) & ( z in Z1 or z = x ) ) by TARSKI:def 1;
assume A20: not [y,z] in T ; :: thesis: contradiction
then not [z,y] in T by EQREL_1:12;
hence contradiction by A18, A19, A20, Def3, Th27; :: thesis: verum

end;

then A21: Z1 \/ {x} is TolSet of T by Def3;
Z1 in bool X by A1, A17;
then ( {x} c= X & Z1 c= X ) by A18, ZFMISC_1:37;
then A22: Z1 \/ {x} c= X by XBOOLE_1:8;
( Y c= Z1 & Z1 c= Z1 \/ {x} ) by A2, A17, XBOOLE_1:7;
then Y c= Z1 \/ {x} by XBOOLE_1:1;
then A23: Z1 \/ {x} in TS by A2, A21, A22;
Z1 \/ {x} <> Z1

proof

assume A24: Z1 \/ {x} = Z1 ; :: thesis: contradiction
x in {x} by TARSKI:def 1;
hence contradiction by A18, A24, XBOOLE_0:def 3; :: thesis: verum

end;

hence contradiction by A17, A23, 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, A17; :: thesis: verum