let X be non empty set ; :: thesis:
let H be covering T_3 Hierarchy of X; :: thesis:
assume that
A1: H is lower-bounded and
A2: not {} in H and
A3: for C1 being set st C1 <> {} & C1 c= PARTITIONS X & ( for P1, P2 being set st P1 in C1 & P2 in C1 & not P1 is_finer_than P2 holds
P2 is_finer_than P1 ) holds
ex PX, PY being set st
( PX in C1 & PY in C1 & ( for PZ being set st PZ in C1 holds
( PZ is_finer_than PY & PX is_finer_than PZ ) ) ) ; :: thesis:
union H = X by ABIAN:4;
then consider h being object such that
A4: h in H by XBOOLE_0:def 1, ZFMISC_1:2;
reconsider h = h as Subset of X by A4;
consider PX being a_partition of X such that
h in PX and
A5: PX c= H by A1, A2, A4, Th16;
set L = {PX};
A6: {PX} c= PARTITIONS X

let l be object ; :: according to TARSKI:def 3 :: thesis:
assume l in {PX} ; :: thesis:
then l = PX by TARSKI:def 1;
hence l in PARTITIONS X by PARTIT1:def 3; :: thesis:

end;

A7: now :: thesis:

let P1, P2 be set ; :: thesis:
assume that
A8: P1 in {PX} and
A9: P2 in {PX} ; :: thesis:
P1 = PX by A8, TARSKI:def 1;
hence ( P1 is_finer_than P2 or P2 is_finer_than P1 ) by A9, TARSKI:def 1; :: thesis:

end;

A10: H is hierarchic by Def4;
defpred S₁[ set ] means ( ( for P being set st P in $1 holds
P c= H ) & ( for P1, P2 being set st P1 in $1 & P2 in $1 & not P1 is_finer_than P2 holds
P2 is_finer_than P1 ) );
consider RL being set such that
A11: for L being set holds
( L in RL iff ( L in bool (PARTITIONS X) & S₁[L] ) ) from XFAMILY:sch 1();
for a being set st a in {PX} holds
a c= H by A5, TARSKI:def 1;
then A12: {PX} in RL by A11, A6, A7;

now :: thesis:

let Z be set ; :: thesis:
assume that
A13: Z c= RL and
A14: Z is c=-linear ; :: thesis:
set Y = union Z;
A15: for X1, X2 being set st X1 in Z & X2 in Z & not X1 c= X2 holds
X2 c= X1 by XBOOLE_0:def 9, A14, ORDINAL1:def 8;

A16: now :: thesis:

let P1, P2 be set ; :: thesis:
assume that
A17: P1 in union Z and
A18: P2 in union Z ; :: thesis:
consider L1 being set such that
A19: P1 in L1 and
A20: L1 in Z by A17, TARSKI:def 4;
consider L2 being set such that
A21: P2 in L2 and
A22: L2 in Z by A18, TARSKI:def 4;

per cases by A15, A20, A22;

suppose L1 c= L2 ; :: thesis:

hence ( P1 is_finer_than P2 or P2 is_finer_than P1 ) by A11, A13, A19, A21, A22; :: thesis:

end;

suppose L2 c= L1 ; :: thesis:

hence ( P1 is_finer_than P2 or P2 is_finer_than P1 ) by A11, A13, A19, A20, A21; :: thesis:

end;

take Y = union Z; :: thesis:

A23: now :: thesis:

let P be set ; :: thesis:
assume P in Y ; :: thesis:
then ex L3 being set st
( P in L3 & L3 in Z ) by TARSKI:def 4;
hence P c= H by A11, A13; :: thesis:

end;

Y c= PARTITIONS X

proof

let P be object ; :: according to TARSKI:def 3 :: thesis:
assume P in Y ; :: thesis:
then consider L4 being set such that
A24: P in L4 and
A25: L4 in Z by TARSKI:def 4;
L4 in bool (PARTITIONS X) by A11, A13, A25;
hence P in PARTITIONS X by A24; :: thesis:

end;

hence Y in RL by A11, A23, A16; :: thesis:
thus for X1 being set st X1 in Z holds
X1 c= Y by ZFMISC_1:74; :: thesis:

end;

then consider C being set such that
A26: C in RL and
A27: for Z being set st Z in RL & Z <> C holds
not C c= Z by A12, ORDERS_1:65;
reconsider C = C as Subset of (PARTITIONS X) by A11, A26;
A28: C is Classification of X

proof

let P1, P2 be a_partition of X; :: according to TAXONOM1:def 1 :: thesis:
assume that
A29: P1 in C and
A30: P2 in C ; :: thesis:
thus ( P1 is_finer_than P2 or P2 is_finer_than P1 ) by A11, A26, A29, A30; :: thesis:

end;

A31: C <> {} by A12, A27, XBOOLE_1:2;
A32: H c= union C

proof

let h be object ; :: according to TARSKI:def 3 :: thesis:
assume A33: h in H ; :: thesis:
reconsider hh = h as set by TARSKI:1;

per cases ;

suppose A34: not h in union C ; :: thesis:

defpred S₂[ set ] means ex hx being set st
( hx in $1 & hh c= hx & h <> hx );
consider Ca being set such that
A35: for p being set holds
( p in Ca iff ( p in C & S₂[p] ) ) from XFAMILY:sch 1();
A36: Ca c= C by A35;
defpred S₃[ set ] means ex hx being set st
( hx in $1 & hx c= hh & h <> hx );
consider Cb being set such that
A37: for p being set holds
( p in Cb iff ( p in C & S₃[p] ) ) from XFAMILY:sch 1();
consider PS being a_partition of X such that
A38: h in PS and
A39: PS c= H by A1, A2, A33, Th16;
A40: h <> {} by A38, EQREL_1:def 4;

A41: now :: thesis:

consider t being object such that
A42: t in hh by A40, XBOOLE_0:def 1;
let p be set ; :: thesis:
assume p in C ; :: thesis:
then p is a_partition of X by PARTIT1:def 3;
then union p = X by EQREL_1:def 4;
then consider v being set such that
A43: t in v and
A44: v in p by A33, A42, TARSKI:def 4;
assume A45: for hv being set st hv in p holds
hv misses hh ; :: thesis:
not v misses hh by A42, A43, XBOOLE_0:3;
hence contradiction by A45, A44; :: thesis:

end;

A46: C c= Ca \/ Cb

proof

let p be object ; :: according to TARSKI:def 3 :: thesis:
assume A47: p in C ; :: thesis:
reconsider pp = p as set by TARSKI:1;
consider hv being set such that
A48: hv in pp and
A49: not hv misses hh by A41, A47;
A50: h <> hv by A34, A47, A48, TARSKI:def 4;
A51: pp c= H by A11, A26, A47;

per cases by A10, A33, A48, A49, A51;

suppose hv c= hh ; :: thesis:

then p in Cb by A37, A47, A48, A50;
hence p in Ca \/ Cb by XBOOLE_0:def 3; :: thesis:

end;

suppose hh c= hv ; :: thesis:

then p in Ca by A35, A47, A48, A50;
hence p in Ca \/ Cb by XBOOLE_0:def 3; :: thesis:

end;

Cb c= C by A37;
then Ca \/ Cb c= C by A36, XBOOLE_1:8;
then A52: C = Ca \/ Cb by A46, XBOOLE_0:def 10;
then A53: Ca c= C by XBOOLE_1:7;

A54: now :: thesis:

let P1, P2 be set ; :: thesis:
assume that
A55: P1 in Ca and
A56: P2 in Ca ; :: thesis:
P2 in C by A53, A56;
then A57: P2 is a_partition of X by PARTIT1:def 3;
P1 in C by A53, A55;
then P1 is a_partition of X by PARTIT1:def 3;
hence ( P1 is_finer_than P2 or P2 is_finer_than P1 ) by A28, A53, A55, A56, A57, TAXONOM1:def 1; :: thesis:

end;

A58: Cb c= C by A52, XBOOLE_1:7;

A59: now :: thesis:

let P1, P2 be set ; :: thesis:
assume that
A60: P1 in Cb and
A61: P2 in Cb ; :: thesis:
P2 in C by A58, A61;
then A62: P2 is a_partition of X by PARTIT1:def 3;
P1 in C by A58, A60;
then P1 is a_partition of X by PARTIT1:def 3;
hence ( P1 is_finer_than P2 or P2 is_finer_than P1 ) by A28, A58, A60, A61, A62, TAXONOM1:def 1; :: thesis:

end;

now :: thesis:

per cases ;

suppose A63: Cb <> {} ; :: thesis:

defpred S₄[ set ] means $1 misses hh;
A64: {h} c= H by A33, TARSKI:def 1;
consider PX, Pmax being set such that
PX in Cb and
A65: Pmax in Cb and
A66: for PZ being set st PZ in Cb holds
( PZ is_finer_than Pmax & PX is_finer_than PZ ) by A3, A58, A59, A63, XBOOLE_1:1;
consider Pb being set such that
A67: for x being set holds
( x in Pb iff ( x in Pmax & S₄[x] ) ) from XFAMILY:sch 1();
set PS1 = Pb \/ {h};
set C1 = C \/ {(Pb \/ {h})};
Pmax in C by A58, A65;
then A68: Pmax is a_partition of X by PARTIT1:def 3;
A69: Pmax c= H by A11, A26, A58, A65;
then A70: for a being set holds
( not a in Pmax or a c= hh or hh c= a or hh misses a ) by A10, A33;
Pb c= Pmax by A67;
then Pb c= H by A69;
then A71: Pb \/ {h} c= H by A64, XBOOLE_1:8;

A72: now :: thesis:

let P3 be set ; :: thesis:
assume A73: P3 in C \/ {(Pb \/ {h})} ; :: thesis:

per cases by A73, XBOOLE_0:def 3;

suppose P3 in C ; :: thesis:

hence P3 c= H by A11, A26; :: thesis:

end;

suppose P3 in {(Pb \/ {h})} ; :: thesis:

hence P3 c= H by A71, TARSKI:def 1; :: thesis:

end;

Pb \/ {h} in {(Pb \/ {h})} by TARSKI:def 1;
then A74: Pb \/ {h} in C \/ {(Pb \/ {h})} by XBOOLE_0:def 3;
h in {h} by TARSKI:def 1;
then A75: h in Pb \/ {h} by XBOOLE_0:def 3;
A76: ex hx being set st
( hx in Pmax & hx c= hh & hh <> hx ) by A37, A65;
then A77: Pmax is_finer_than Pb \/ {h} by A33, A40, A68, A67, A70, Th18;

A78: now :: thesis:

let P3 be set ; :: thesis:
assume A79: P3 in C ; :: thesis:

per cases ;

suppose Ca = {} ; :: thesis:

then P3 is_finer_than Pmax by A46, A66, A79;
hence ( Pb \/ {h} is_finer_than P3 or P3 is_finer_than Pb \/ {h} ) by A77, SETFAM_1:17; :: thesis:

end;

suppose A80: Ca <> {} ; :: thesis:

now :: thesis:

per cases by A46, A79, XBOOLE_0:def 3;

suppose A81: P3 in Ca ; :: thesis:

consider Pmin, PY being set such that
A82: Pmin in Ca and
PY in Ca and
A83: for PZ being set st PZ in Ca holds
( PZ is_finer_than PY & Pmin is_finer_than PZ ) by A3, A53, A54, A80, XBOOLE_1:1;
A84: Pmin is_finer_than P3 by A81, A83;

A85: now :: thesis:

consider hx being set such that
A86: hx in Pmin and
A87: hh c= hx and
A88: h <> hx by A35, A82;
assume Pmin is_finer_than Pmax ; :: thesis:
then consider hz being set such that
A89: hz in Pmax and
A90: hx c= hz by A86;
consider hy being set such that
A91: hy in Pmax and
A92: hy c= hh and
h <> hy by A37, A65;
A93: not hy is empty by A68, A91, EQREL_1:def 4;
hy c= hx by A87, A92;
then hy meets hz by A90, A93, Lm5, XBOOLE_1:1;
then hy = hz by A68, A91, A89, EQREL_1:def 4;
then hx c= hh by A92, A90;
hence contradiction by A87, A88, XBOOLE_0:def 10; :: thesis:

end;

A94: Pmax in C by A52, A65, XBOOLE_0:def 3;
then A95: Pmax is a_partition of X by PARTIT1:def 3;
Pmin in C by A53, A82;
then A96: Pmin is a_partition of X by PARTIT1:def 3;
A97: ex hw being set st
( hw in Pmin & hh c= hw & h <> hw ) by A35, A82;
A98: Pmin in C by A52, A82, XBOOLE_0:def 3;
then Pmin is a_partition of X by PARTIT1:def 3;
then Pmax is_finer_than Pmin by A28, A98, A94, A95, A85, TAXONOM1:def 1;
then Pb \/ {h} is_finer_than Pmin by A33, A40, A68, A67, A70, A76, A96, A97, Th18;
hence ( Pb \/ {h} is_finer_than P3 or P3 is_finer_than Pb \/ {h} ) by A84, SETFAM_1:17; :: thesis:

end;

suppose P3 in Cb ; :: thesis:

then P3 is_finer_than Pmax by A66;
hence ( Pb \/ {h} is_finer_than P3 or P3 is_finer_than Pb \/ {h} ) by A77, SETFAM_1:17; :: thesis:

end;

hence ( Pb \/ {h} is_finer_than P3 or P3 is_finer_than Pb \/ {h} ) ; :: thesis:

end;

A99: now :: thesis:

let P1, P2 be set ; :: thesis:
assume that
A100: P1 in C \/ {(Pb \/ {h})} and
A101: P2 in C \/ {(Pb \/ {h})} ; :: thesis:

per cases by A100, XBOOLE_0:def 3;

suppose A102: P1 in C ; :: thesis:

per cases by A101, XBOOLE_0:def 3;

suppose A103: P2 in C ; :: thesis:

then A104: P2 is a_partition of X by PARTIT1:def 3;
P1 is a_partition of X by A102, PARTIT1:def 3;
hence ( P1 is_finer_than P2 or P2 is_finer_than P1 ) by A28, A102, A103, A104, TAXONOM1:def 1; :: thesis:

end;

suppose P2 in {(Pb \/ {h})} ; :: thesis:

then P2 = Pb \/ {h} by TARSKI:def 1;
hence ( P1 is_finer_than P2 or P2 is_finer_than P1 ) by A78, A102; :: thesis:

end;

suppose P1 in {(Pb \/ {h})} ; :: thesis:

then A105: P1 = Pb \/ {h} by TARSKI:def 1;

per cases by A101, XBOOLE_0:def 3;

suppose P2 in C ; :: thesis:

hence ( P1 is_finer_than P2 or P2 is_finer_than P1 ) by A78, A105; :: thesis:

end;

suppose P2 in {(Pb \/ {h})} ; :: thesis:

hence ( P1 is_finer_than P2 or P2 is_finer_than P1 ) by A105, TARSKI:def 1; :: thesis:

end;

A106: Pb \/ {h} is a_partition of X by A33, A40, A68, A67, A70, A76, Th18;
{(Pb \/ {h})} c= PARTITIONS X

proof

let s be object ; :: according to TARSKI:def 3 :: thesis:
assume s in {(Pb \/ {h})} ; :: thesis:
then s = Pb \/ {h} by TARSKI:def 1;
hence s in PARTITIONS X by A106, PARTIT1:def 3; :: thesis:

end;

then C \/ {(Pb \/ {h})} c= PARTITIONS X by XBOOLE_1:8;
then C \/ {(Pb \/ {h})} in RL by A11, A72, A99;
then C = C \/ {(Pb \/ {h})} by A27, XBOOLE_1:7;
hence h in union C by A75, A74, TARSKI:def 4; :: thesis:

end;

suppose A107: Cb = {} ; :: thesis:

then consider Pmin, PY being set such that
A108: Pmin in Ca and
PY in Ca and
A109: for PZ being set st PZ in Ca holds
( PZ is_finer_than PY & Pmin is_finer_than PZ ) by A3, A31, A52, A54;
consider hw being set such that
A110: hw in Pmin and
A111: hh c= hw and
hh <> hw by A35, A108;
defpred S₄[ set ] means $1 c= hw;
consider PT being set such that
A112: for a being set holds
( a in PT iff ( a in PS & S₄[a] ) ) from XFAMILY:sch 1();
set PS1 = PT \/ (Pmin \ {hw});
set C1 = C \/ {(PT \/ (Pmin \ {hw}))};
PT c= PS by A112;
then A113: PT c= H by A39;
A114: Pmin c= H by A11, A26, A53, A108;
then Pmin \ {hw} c= H ;
then A115: PT \/ (Pmin \ {hw}) c= H by A113, XBOOLE_1:8;

A116: now :: thesis:

let P3 be set ; :: thesis:
assume A117: P3 in C \/ {(PT \/ (Pmin \ {hw}))} ; :: thesis:

per cases by A117, XBOOLE_0:def 3;

suppose P3 in C ; :: thesis:

hence P3 c= H by A11, A26; :: thesis:

end;

suppose P3 in {(PT \/ (Pmin \ {hw}))} ; :: thesis:

hence P3 c= H by A115, TARSKI:def 1; :: thesis:

end;

Pmin in C by A53, A108;
then A118: Pmin is a_partition of X by PARTIT1:def 3;
A119: for a being set holds
( not a in PS or a c= hw or hw c= a or hw misses a ) by A10, A39, A114, A110;
then A120: PT \/ (Pmin \ {hw}) is_finer_than Pmin by A38, A40, A118, A110, A111, A112, Th17;

A121: now :: thesis:

let P3 be set ; :: thesis:
assume P3 in C ; :: thesis:
then Pmin is_finer_than P3 by A46, A107, A109;
hence ( PT \/ (Pmin \ {hw}) is_finer_than P3 or P3 is_finer_than PT \/ (Pmin \ {hw}) ) by A120, SETFAM_1:17; :: thesis:

end;

A122: now :: thesis:

let P1, P2 be set ; :: thesis:
assume that
A123: P1 in C \/ {(PT \/ (Pmin \ {hw}))} and
A124: P2 in C \/ {(PT \/ (Pmin \ {hw}))} ; :: thesis:

per cases by A123, XBOOLE_0:def 3;

suppose A125: P1 in C ; :: thesis:

per cases by A124, XBOOLE_0:def 3;

suppose A126: P2 in C ; :: thesis:

then A127: P2 is a_partition of X by PARTIT1:def 3;
P1 is a_partition of X by A125, PARTIT1:def 3;
hence ( P1 is_finer_than P2 or P2 is_finer_than P1 ) by A28, A125, A126, A127, TAXONOM1:def 1; :: thesis:

end;

suppose P2 in {(PT \/ (Pmin \ {hw}))} ; :: thesis:

then P2 = PT \/ (Pmin \ {hw}) by TARSKI:def 1;
hence ( P1 is_finer_than P2 or P2 is_finer_than P1 ) by A121, A125; :: thesis:

end;

suppose P1 in {(PT \/ (Pmin \ {hw}))} ; :: thesis:

then A128: P1 = PT \/ (Pmin \ {hw}) by TARSKI:def 1;

per cases by A124, XBOOLE_0:def 3;

suppose P2 in C ; :: thesis:

hence ( P1 is_finer_than P2 or P2 is_finer_than P1 ) by A121, A128; :: thesis:

end;

suppose P2 in {(PT \/ (Pmin \ {hw}))} ; :: thesis:

hence ( P1 is_finer_than P2 or P2 is_finer_than P1 ) by A128, TARSKI:def 1; :: thesis:

end;

A129: PT \/ (Pmin \ {hw}) is a_partition of X by A38, A40, A118, A110, A111, A112, A119, Th17;
{(PT \/ (Pmin \ {hw}))} c= PARTITIONS X

proof

let s be object ; :: according to TARSKI:def 3 :: thesis:
assume s in {(PT \/ (Pmin \ {hw}))} ; :: thesis:
then s = PT \/ (Pmin \ {hw}) by TARSKI:def 1;
hence s in PARTITIONS X by A129, PARTIT1:def 3; :: thesis:

end;

then C \/ {(PT \/ (Pmin \ {hw}))} c= PARTITIONS X by XBOOLE_1:8;
then C \/ {(PT \/ (Pmin \ {hw}))} in RL by A11, A116, A122;
then A130: C = C \/ {(PT \/ (Pmin \ {hw}))} by A27, XBOOLE_1:7;
A131: PT c= PT \/ (Pmin \ {hw}) by XBOOLE_1:7;
A132: PT \/ (Pmin \ {hw}) in {(PT \/ (Pmin \ {hw}))} by TARSKI:def 1;
A133: {(PT \/ (Pmin \ {hw}))} c= C \/ {(PT \/ (Pmin \ {hw}))} by XBOOLE_1:7;
h in PT by A38, A111, A112;
hence h in union C by A131, A133, A132, A130, TARSKI:def 4; :: thesis:

end;

hence h in union C ; :: thesis:

end;

suppose h in union C ; :: thesis:

hence h in union C ; :: thesis:

end;

take C ; :: thesis:
union C c= H

proof

let h be object ; :: according to TARSKI:def 3 :: thesis:
assume h in union C ; :: thesis:
then consider P being set such that
A134: h in P and
A135: P in C by TARSKI:def 4;
P c= H by A11, A26, A135;
hence h in H by A134; :: thesis:

end;

hence ( C is Classification of X & union C = H ) by A28, A32, XBOOLE_0:def 10; :: thesis: