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 set 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, Th17;
set L = {PX};
A6: {PX} c= PARTITIONS X

let l be set ; :: 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

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 XBOOLE_0: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

let Z be set ; :: thesis:
assume that
A13: Z c= RL and
A14: Z is c=-linear ; :: thesis:
set Y = union Z;

A15: now

let X1, X2 be set ; :: thesis:
assume that
A16: X1 in Z and
A17: X2 in Z ; :: thesis:
X1,X2 are_c=-comparable by A14, A16, A17, ORDINAL1:def 8;
hence ( X1 c= X2 or X2 c= X1 ) by XBOOLE_0:def 9; :: thesis:

end;

A18: now

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

per cases by A15, A22, A24;

suppose L1 c= L2 ; :: thesis:

hence ( P1 is_finer_than P2 or P2 is_finer_than P1 ) by A11, A13, A21, A23, A24; :: thesis:

end;

suppose L2 c= L1 ; :: thesis:

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

end;

take Y = union Z; :: thesis:

A25: now

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 set ; :: according to TARSKI:def 3 :: thesis:
assume P in Y ; :: thesis:
then consider L4 being set such that
A26: P in L4 and
A27: L4 in Z by TARSKI:def 4;
L4 in bool (PARTITIONS X) by A11, A13, A27;
hence P in PARTITIONS X by A26; :: thesis:

end;

hence Y in RL by A11, A25, A18; :: 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
A28: C in RL and
A29: 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, A28;
A30: C is Classification of X

proof

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

end;

A33: C <> {} by A12, A29, XBOOLE_1:2;
A34: H c= union C

proof

let h be set ; :: according to TARSKI:def 3 :: thesis:
assume A35: h in H ; :: thesis:

per cases ;

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

defpred S₂[ set ] means ex hx being set st
( hx in $1 & h c= hx & h <> hx );
consider Ca being set such that
A37: for p being set holds
( p in Ca iff ( p in C & S₂[p] ) ) from XBOOLE_0:sch 1();
A38: Ca c= C

proof

let s be set ; :: according to TARSKI:def 3 :: thesis:
assume s in Ca ; :: thesis:
hence s in C by A37; :: thesis:

end;

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

A43: now

consider t being set such that
A44: t in h by A42, 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
A45: t in v and
A46: v in p by A35, A44, TARSKI:def 4;
assume A47: for hv being set st hv in p holds
hv misses h ; :: thesis:
not v misses h by A44, A45, XBOOLE_0:3;
hence contradiction by A47, A46; :: thesis:

end;

A48: C c= Ca \/ Cb

proof

let p be set ; :: according to TARSKI:def 3 :: thesis:
assume A49: p in C ; :: thesis:
consider hv being set such that
A50: hv in p and
A51: not hv misses h by A43, A49;
A52: h <> hv by A36, A49, A50, TARSKI:def 4;
A53: p c= H by A11, A28, A49;

per cases by A10, A35, A50, A51, A53, Def3;

suppose hv c= h ; :: thesis:

then p in Cb by A39, A49, A50, A52;
hence p in Ca \/ Cb by XBOOLE_0:def 3; :: thesis:

end;

suppose h c= hv ; :: thesis:

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

end;

Cb c= C

proof

let s be set ; :: according to TARSKI:def 3 :: thesis:
assume s in Cb ; :: thesis:
hence s in C by A39; :: thesis:

end;

then Ca \/ Cb c= C by A38, XBOOLE_1:8;
then A54: C = Ca \/ Cb by A48, XBOOLE_0:def 10;
then A55: Ca c= C by XBOOLE_1:7;

A56: now

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

end;

A60: Cb c= C by A54, XBOOLE_1:7;

A61: now

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

end;

now

per cases ;

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

defpred S₄[ set ] means $1 misses h;
A66: {h} c= H

proof

let s be set ; :: according to TARSKI:def 3 :: thesis:
assume s in {h} ; :: thesis:
hence s in H by A35, TARSKI:def 1; :: thesis:

end;

consider PX, Pmax being set such that
PX in Cb and
A67: Pmax in Cb and
A68: for PZ being set st PZ in Cb holds
( PZ is_finer_than Pmax & PX is_finer_than PZ ) by A3, A60, A61, A65, XBOOLE_1:1;
consider Pb being set such that
A69: for x being set holds
( x in Pb iff ( x in Pmax & S₄[x] ) ) from XBOOLE_0:sch 1();
set PS1 = Pb \/ {h};
set C1 = C \/ {(Pb \/ {h})};
Pmax in C by A60, A67;
then A70: Pmax is a_partition of X by PARTIT1:def 3;
A71: Pmax c= H by A11, A28, A60, A67;
then A72: for a being set holds
( not a in Pmax or a c= h or h c= a or h misses a ) by A10, A35, Def3;
Pb c= Pmax

proof

let s be set ; :: according to TARSKI:def 3 :: thesis:
assume s in Pb ; :: thesis:
hence s in Pmax by A69; :: thesis:

end;

then Pb c= H by A71, XBOOLE_1:1;
then A73: Pb \/ {h} c= H by A66, XBOOLE_1:8;

A74: now

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

per cases by A75, XBOOLE_0:def 3;

suppose P3 in C ; :: thesis:

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

end;

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

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

end;

Pb \/ {h} in {(Pb \/ {h})} by TARSKI:def 1;
then A76: Pb \/ {h} in C \/ {(Pb \/ {h})} by XBOOLE_0:def 3;
h in {h} by TARSKI:def 1;
then A77: h in Pb \/ {h} by XBOOLE_0:def 3;
A78: ex hx being set st
( hx in Pmax & hx c= h & h <> hx ) by A39, A67;
then A79: Pmax is_finer_than Pb \/ {h} by A35, A42, A70, A69, A72, Th19;

A80: now

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

per cases ;

suppose Ca = {} ; :: thesis:

then P3 is_finer_than Pmax by A48, A68, A81;
hence ( Pb \/ {h} is_finer_than P3 or P3 is_finer_than Pb \/ {h} ) by A79, SETFAM_1:17; :: thesis:

end;

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

now

per cases by A48, A81, XBOOLE_0:def 3;

suppose A83: P3 in Ca ; :: thesis:

consider Pmin, PY being set such that
A84: Pmin in Ca and
PY in Ca and
A85: for PZ being set st PZ in Ca holds
( PZ is_finer_than PY & Pmin is_finer_than PZ ) by A3, A55, A56, A82, XBOOLE_1:1;
A86: Pmin is_finer_than P3 by A83, A85;

A87: now

consider hx being set such that
A88: hx in Pmin and
A89: h c= hx and
A90: h <> hx by A37, A84;
assume Pmin is_finer_than Pmax ; :: thesis:
then consider hz being set such that
A91: hz in Pmax and
A92: hx c= hz by A88, SETFAM_1:def 2;
consider hy being set such that
A93: hy in Pmax and
A94: hy c= h and
h <> hy by A39, A67;
A95: not hy is empty by A70, A93, EQREL_1:def 4;
hy c= hx by A89, A94, XBOOLE_1:1;
then hy meets hz by A92, A95, Lm4, XBOOLE_1:1;
then hy = hz by A70, A93, A91, EQREL_1:def 4;
then hx c= h by A94, A92, XBOOLE_1:1;
hence contradiction by A89, A90, XBOOLE_0:def 10; :: thesis:

end;

A96: Pmax in C by A54, A67, XBOOLE_0:def 3;
then A97: Pmax is a_partition of X by PARTIT1:def 3;
Pmin in C by A55, A84;
then A98: Pmin is a_partition of X by PARTIT1:def 3;
A99: ex hw being set st
( hw in Pmin & h c= hw & h <> hw ) by A37, A84;
A100: Pmin in C by A54, A84, XBOOLE_0:def 3;
then Pmin is a_partition of X by PARTIT1:def 3;
then Pmax is_finer_than Pmin by A30, A100, A96, A97, A87, TAXONOM1:def 1;
then Pb \/ {h} is_finer_than Pmin by A35, A42, A70, A69, A72, A78, A98, A99, Th19;
hence ( Pb \/ {h} is_finer_than P3 or P3 is_finer_than Pb \/ {h} ) by A86, SETFAM_1:17; :: thesis:

end;

suppose P3 in Cb ; :: thesis:

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

end;

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

end;

A101: now

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

per cases by A102, XBOOLE_0:def 3;

suppose A104: P1 in C ; :: thesis:

per cases by A103, XBOOLE_0:def 3;

suppose A105: P2 in C ; :: thesis:

then A106: P2 is a_partition of X by PARTIT1:def 3;
P1 is a_partition of X by A104, PARTIT1:def 3;
hence ( P1 is_finer_than P2 or P2 is_finer_than P1 ) by A30, A104, A105, A106, 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 A80, A104; :: thesis:

end;

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

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

per cases by A103, XBOOLE_0:def 3;

suppose P2 in C ; :: thesis:

hence ( P1 is_finer_than P2 or P2 is_finer_than P1 ) by A80, A107; :: thesis:

end;

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

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

end;

A108: Pb \/ {h} is a_partition of X by A35, A42, A70, A69, A72, A78, Th19;
{(Pb \/ {h})} c= PARTITIONS X

proof

let s be set ; :: 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 A108, PARTIT1:def 3; :: thesis:

end;

then C \/ {(Pb \/ {h})} c= PARTITIONS X by XBOOLE_1:8;
then C \/ {(Pb \/ {h})} in RL by A11, A74, A101;
then C = C \/ {(Pb \/ {h})} by A29, XBOOLE_1:7;
hence h in union C by A77, A76, TARSKI:def 4; :: thesis:

end;

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

then consider Pmin, PY being set such that
A110: Pmin in Ca and
PY in Ca and
A111: for PZ being set st PZ in Ca holds
( PZ is_finer_than PY & Pmin is_finer_than PZ ) by A3, A33, A54, A56;
consider hw being set such that
A112: hw in Pmin and
A113: h c= hw and
h <> hw by A37, A110;
defpred S₄[ set ] means $1 c= hw;
consider PT being set such that
A114: for a being set holds
( a in PT iff ( a in PS & S₄[a] ) ) from XBOOLE_0:sch 1();
set PS1 = PT \/ (Pmin \ {hw});
set C1 = C \/ {(PT \/ (Pmin \ {hw}))};
PT c= PS

proof

let s be set ; :: according to TARSKI:def 3 :: thesis:
assume s in PT ; :: thesis:
hence s in PS by A114; :: thesis:

end;

then A115: PT c= H by A41, XBOOLE_1:1;
A116: Pmin c= H by A11, A28, A55, A110;
then Pmin \ {hw} c= H by XBOOLE_1:1;
then A117: PT \/ (Pmin \ {hw}) c= H by A115, XBOOLE_1:8;

A118: now

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

per cases by A119, XBOOLE_0:def 3;

suppose P3 in C ; :: thesis:

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

end;

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

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

end;

Pmin in C by A55, A110;
then A120: Pmin is a_partition of X by PARTIT1:def 3;
A121: for a being set holds
( not a in PS or a c= hw or hw c= a or hw misses a ) by A10, A41, A116, A112, Def3;
then A122: PT \/ (Pmin \ {hw}) is_finer_than Pmin by A40, A42, A120, A112, A113, A114, Th18;

A123: now

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

end;

A124: now

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

per cases by A125, XBOOLE_0:def 3;

suppose A127: P1 in C ; :: thesis:

per cases by A126, XBOOLE_0:def 3;

suppose A128: P2 in C ; :: thesis:

then A129: P2 is a_partition of X by PARTIT1:def 3;
P1 is a_partition of X by A127, PARTIT1:def 3;
hence ( P1 is_finer_than P2 or P2 is_finer_than P1 ) by A30, A127, A128, A129, 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 A123, A127; :: thesis:

end;

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

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

per cases by A126, XBOOLE_0:def 3;

suppose P2 in C ; :: thesis:

hence ( P1 is_finer_than P2 or P2 is_finer_than P1 ) by A123, A130; :: thesis:

end;

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

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

end;

A131: PT \/ (Pmin \ {hw}) is a_partition of X by A40, A42, A120, A112, A113, A114, A121, Th18;
{(PT \/ (Pmin \ {hw}))} c= PARTITIONS X

proof

let s be set ; :: 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 A131, 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, A118, A124;
then A132: C = C \/ {(PT \/ (Pmin \ {hw}))} by A29, XBOOLE_1:7;
A133: PT c= PT \/ (Pmin \ {hw}) by XBOOLE_1:7;
A134: PT \/ (Pmin \ {hw}) in {(PT \/ (Pmin \ {hw}))} by TARSKI:def 1;
A135: {(PT \/ (Pmin \ {hw}))} c= C \/ {(PT \/ (Pmin \ {hw}))} by XBOOLE_1:7;
h in PT by A40, A113, A114;
hence h in union C by A133, A135, A134, A132, 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 set ; :: according to TARSKI:def 3 :: thesis:
assume h in union C ; :: thesis:
then consider P being set such that
A136: h in P and
A137: P in C by TARSKI:def 4;
P c= H by A11, A28, A137;
hence h in H by A136; :: thesis:

end;

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