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 XFAMILY:sch 1();
A2:
TS c= bool X
by A1;
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 ;
( 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
;
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 ;
( 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
;
[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;
verum
end;
then A12:
union Z is
TolSet of
T
by Def1;
take
union Z
;
( union Z in TS & ( for X1 being set st X1 in Z holds
X1 c= 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;
for X1 being set st X1 in Z holds
X1 c= union Z
let X1 be
set ;
( X1 in Z implies X1 c= union Z )
assume
X1 in Z
;
X1 c= union Z
hence
X1 c= union Z
by ZFMISC_1:74;
verum
end;
( {} c= X & {} is TolSet of T )
by Th12;
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
; Y is TolClass-like
let x be set ; TOLER_1:def 2 ( 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
; 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
; 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 ;
( 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}
;
[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
;
contradiction
then
not
[z,y] in T
by EQREL_1:6;
hence
contradiction
by A16, A18, A21, A22, A23, Def1, Th7;
verum
end;
then A24:
Y \/ {x} is TolSet of T
by Def1;
A25:
Y \/ {x} <> Y
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; verum