let X be set ; 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; for Y being TolSet of T ex Z being TolClass of T st Y c= Z
let Y be TolSet of T; 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 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 ) )
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 ;
( 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
;
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 ;
( 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
;
[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;
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 ) ) )
(
Z = {} implies ex
Y being
set st
(
Y in TS & ( for
X1 being
set st
X1 in Z holds
X1 c= Y ) ) )
hence
ex
Y being
set st
(
Y in TS & ( for
X1 being
set st
X1 in Z holds
X1 c= Y ) )
by A15;
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
;
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 ;
( 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}
;
[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
;
contradiction
then
not
[z,y] in T
by EQREL_1:6;
hence
contradiction
by A24, A25, A29, A30, A31, Def1, Th7;
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
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;
verum
end;
then reconsider Z1 = Z1 as TolClass of T ;
take
Z1
; Y c= Z1
thus
Y c= Z1
by A2, A21; verum