let X be non empty set ; :: thesis: for H being covering T_3 Hierarchy of X st H is lower-bounded & not {} in H & ( 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 ) ) ) ) holds
ex C being Classification of X st union C = H

let H be covering T_3 Hierarchy of X; :: thesis: ( H is lower-bounded & not {} in H & ( 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 ) ) ) ) implies ex C being Classification of X st union C = H )

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: ex C being Classification of X st union C = H
union H = X by ABIAN:4;
then consider h being object such that
A4: h in H by ;
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
proof
let l be object ; :: according to TARSKI:def 3 :: thesis: ( not l in {PX} or l in PARTITIONS X )
assume l in {PX} ; :: thesis:
then l = PX by TARSKI:def 1;
hence l in PARTITIONS X by PARTIT1:def 3; :: thesis: verum
end;
A7: now :: thesis: for P1, P2 being set st P1 in {PX} & P2 in {PX} & not P1 is_finer_than P2 holds
P2 is_finer_than P1
let P1, P2 be set ; :: thesis: ( P1 in {PX} & P2 in {PX} & not P1 is_finer_than P2 implies P2 is_finer_than P1 )
assume that
A8: P1 in {PX} and
A9: P2 in {PX} ; :: thesis: ( P1 is_finer_than P2 or P2 is_finer_than P1 )
P1 = PX by ;
hence ( P1 is_finer_than P2 or P2 is_finer_than P1 ) by ; :: thesis: verum
end;
A10: H is hierarchic by Def4;
defpred S1[ 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 () & S1[L] ) ) from for a being set st a in {PX} holds
a c= H by ;
then A12: {PX} in RL by A11, A6, A7;
now :: thesis: for Z being set st Z c= RL & Z is c=-linear holds
ex Y being set st
( Y in RL & ( for X1 being set st X1 in Z holds
X1 c= Y ) )
let Z be set ; :: thesis: ( Z c= RL & Z is c=-linear implies ex Y being set st
( Y in RL & ( for X1 being set st X1 in Z holds
X1 c= Y ) ) )

assume that
A13: Z c= RL and
A14: Z is c=-linear ; :: thesis: ex Y being set st
( Y in RL & ( for X1 being set st X1 in Z holds
X1 c= Y ) )

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 ;
A16: now :: thesis: for P1, P2 being set st P1 in union Z & P2 in union Z & not P1 is_finer_than P2 holds
P2 is_finer_than P1
let P1, P2 be set ; :: thesis: ( P1 in union Z & P2 in union Z & not b1 is_finer_than b2 implies b2 is_finer_than b1 )
assume that
A17: P1 in union Z and
A18: P2 in union Z ; :: thesis: ( b1 is_finer_than b2 or b2 is_finer_than b1 )
consider L1 being set such that
A19: P1 in L1 and
A20: L1 in Z by ;
consider L2 being set such that
A21: P2 in L2 and
A22: L2 in Z by ;
per cases ( L1 c= L2 or L2 c= L1 ) by ;
end;
end;
take Y = union Z; :: thesis: ( Y in RL & ( for X1 being set st X1 in Z holds
X1 c= Y ) )

A23: now :: thesis: for P being set st P in Y holds
P c= H
let P be set ; :: thesis: ( P in Y implies P c= H )
assume P in Y ; :: thesis: P c= H
then ex L3 being set st
( P in L3 & L3 in Z ) by TARSKI:def 4;
hence P c= H by ; :: thesis: verum
end;
Y c= PARTITIONS X
proof
let P be object ; :: according to TARSKI:def 3 :: thesis: ( not P in Y or P in PARTITIONS X )
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 () by ;
hence P in PARTITIONS X by A24; :: thesis: verum
end;
hence Y in RL by ; :: thesis: for X1 being set st X1 in Z holds
X1 c= Y

thus for X1 being set st X1 in Z holds
X1 c= Y by ZFMISC_1:74; :: thesis: verum
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 ;
reconsider C = C as Subset of () by ;
A28: C is Classification of X
proof
let P1, P2 be a_partition of X; :: according to TAXONOM1:def 1 :: thesis: ( not P1 in C or not P2 in C or P1 is_finer_than P2 or P2 is_finer_than P1 )
assume that
A29: P1 in C and
A30: P2 in C ; :: thesis: ( P1 is_finer_than P2 or P2 is_finer_than P1 )
thus ( P1 is_finer_than P2 or P2 is_finer_than P1 ) by A11, A26, A29, A30; :: thesis: verum
end;
A31: C <> {} by ;
A32: H c= union C
proof
let h be object ; :: according to TARSKI:def 3 :: thesis: ( not h in H or h in union C )
assume A33: h in H ; :: thesis: h in union C
reconsider hh = h as set by TARSKI:1;
per cases ( not h in union C or h in union C ) ;
suppose A34: not h in union C ; :: thesis: h in union C
defpred S2[ 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 & S2[p] ) ) from A36: Ca c= C by A35;
defpred S3[ 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 & S3[p] ) ) from 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 ;
A41: now :: thesis: for p being set st p in C holds
ex hv being set st
( hv in p & not hv misses hh )
consider t being object such that
A42: t in hh by ;
let p be set ; :: thesis: ( p in C implies ex hv being set st
( hv in p & not hv misses hh ) )

assume p in C ; :: thesis: ex hv being set st
( hv in p & not hv misses hh )

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 ;
assume A45: for hv being set st hv in p holds
hv misses hh ; :: thesis: contradiction
not v misses hh by ;
hence contradiction by A45, A44; :: thesis: verum
end;
A46: C c= Ca \/ Cb
proof
let p be object ; :: according to TARSKI:def 3 :: thesis: ( not p in C or p in Ca \/ Cb )
assume A47: p in C ; :: thesis: p in Ca \/ Cb
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 ;
A50: h <> hv by ;
A51: pp c= H by ;
per cases ( hv c= hh or hh c= hv ) by A10, A33, A48, A49, A51;
suppose hv c= hh ; :: thesis: p in Ca \/ Cb
then p in Cb by A37, A47, A48, A50;
hence p in Ca \/ Cb by XBOOLE_0:def 3; :: thesis: verum
end;
suppose hh c= hv ; :: thesis: p in Ca \/ Cb
then p in Ca by A35, A47, A48, A50;
hence p in Ca \/ Cb by XBOOLE_0:def 3; :: thesis: verum
end;
end;
end;
Cb c= C by A37;
then Ca \/ Cb c= C by ;
then A52: C = Ca \/ Cb by ;
then A53: Ca c= C by XBOOLE_1:7;
A54: now :: thesis: for P1, P2 being set st P1 in Ca & P2 in Ca & not P1 is_finer_than P2 holds
P2 is_finer_than P1
let P1, P2 be set ; :: thesis: ( P1 in Ca & P2 in Ca & not P1 is_finer_than P2 implies P2 is_finer_than P1 )
assume that
A55: P1 in Ca and
A56: P2 in Ca ; :: thesis: ( P1 is_finer_than P2 or P2 is_finer_than P1 )
P2 in C by ;
then A57: P2 is a_partition of X by PARTIT1:def 3;
P1 in C by ;
then P1 is a_partition of X by PARTIT1:def 3;
hence ( P1 is_finer_than P2 or P2 is_finer_than P1 ) by ; :: thesis: verum
end;
A58: Cb c= C by ;
A59: now :: thesis: for P1, P2 being set st P1 in Cb & P2 in Cb & not P1 is_finer_than P2 holds
P2 is_finer_than P1
let P1, P2 be set ; :: thesis: ( P1 in Cb & P2 in Cb & not P1 is_finer_than P2 implies P2 is_finer_than P1 )
assume that
A60: P1 in Cb and
A61: P2 in Cb ; :: thesis: ( P1 is_finer_than P2 or P2 is_finer_than P1 )
P2 in C by ;
then A62: P2 is a_partition of X by PARTIT1:def 3;
P1 in C by ;
then P1 is a_partition of X by PARTIT1:def 3;
hence ( P1 is_finer_than P2 or P2 is_finer_than P1 ) by ; :: thesis: verum
end;
now :: thesis: h in union C
per cases ( Cb <> {} or Cb = {} ) ;
suppose A63: Cb <> {} ; :: thesis: h in union C
defpred S4[ set ] means \$1 misses hh;
A64: {h} c= H by ;
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 ;
consider Pb being set such that
A67: for x being set holds
( x in Pb iff ( x in Pmax & S4[x] ) ) from set PS1 = Pb \/ {h};
set C1 = C \/ {(Pb \/ {h})};
Pmax in C by ;
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 ;
Pb c= Pmax by A67;
then Pb c= H by A69;
then A71: Pb \/ {h} c= H by ;
A72: now :: thesis: for P3 being set st P3 in C \/ {(Pb \/ {h})} holds
P3 c= H
let P3 be set ; :: thesis: ( P3 in C \/ {(Pb \/ {h})} implies b1 c= H )
assume A73: P3 in C \/ {(Pb \/ {h})} ; :: thesis: b1 c= H
per cases ( P3 in C or P3 in {(Pb \/ {h})} ) by ;
suppose P3 in C ; :: thesis: b1 c= H
hence P3 c= H by ; :: thesis: verum
end;
suppose P3 in {(Pb \/ {h})} ; :: thesis: b1 c= H
hence P3 c= H by ; :: thesis: verum
end;
end;
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 ;
then A77: Pmax is_finer_than Pb \/ {h} by A33, A40, A68, A67, A70, Th18;
A78: now :: thesis: for P3 being set holds
( not P3 in C or Pb \/ {h} is_finer_than P3 or P3 is_finer_than Pb \/ {h} )
let P3 be set ; :: thesis: ( not P3 in C or Pb \/ {h} is_finer_than b1 or b1 is_finer_than Pb \/ {h} )
assume A79: P3 in C ; :: thesis: ( Pb \/ {h} is_finer_than b1 or b1 is_finer_than Pb \/ {h} )
per cases ( Ca = {} or Ca <> {} ) ;
suppose A80: Ca <> {} ; :: thesis: ( Pb \/ {h} is_finer_than b1 or b1 is_finer_than Pb \/ {h} )
now :: thesis: ( Pb \/ {h} is_finer_than P3 or P3 is_finer_than Pb \/ {h} )
per cases ( P3 in Ca or P3 in Cb ) by ;
suppose A81: P3 in Ca ; :: thesis: ( Pb \/ {h} is_finer_than P3 or P3 is_finer_than Pb \/ {h} )
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 ;
A84: Pmin is_finer_than P3 by ;
A85: now :: thesis: not Pmin is_finer_than Pmax
consider hx being set such that
A86: hx in Pmin and
A87: hh c= hx and
A88: h <> hx by ;
assume Pmin is_finer_than Pmax ; :: thesis: contradiction
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 ;
A93: not hy is empty by ;
hy c= hx by ;
then hy meets hz by ;
then hy = hz by ;
then hx c= hh by ;
hence contradiction by A87, A88, XBOOLE_0:def 10; :: thesis: verum
end;
A94: Pmax in C by ;
then A95: Pmax is a_partition of X by PARTIT1:def 3;
Pmin in C by ;
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 ;
A98: Pmin in C by ;
then Pmin is a_partition of X by PARTIT1:def 3;
then Pmax is_finer_than Pmin by ;
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 ; :: thesis: verum
end;
end;
end;
hence ( Pb \/ {h} is_finer_than P3 or P3 is_finer_than Pb \/ {h} ) ; :: thesis: verum
end;
end;
end;
A99: now :: thesis: for P1, P2 being set st P1 in C \/ {(Pb \/ {h})} & P2 in C \/ {(Pb \/ {h})} & not P1 is_finer_than P2 holds
P2 is_finer_than P1
let P1, P2 be set ; :: thesis: ( P1 in C \/ {(Pb \/ {h})} & P2 in C \/ {(Pb \/ {h})} & not b1 is_finer_than b2 implies b2 is_finer_than b1 )
assume that
A100: P1 in C \/ {(Pb \/ {h})} and
A101: P2 in C \/ {(Pb \/ {h})} ; :: thesis: ( b1 is_finer_than b2 or b2 is_finer_than b1 )
per cases ( P1 in C or P1 in {(Pb \/ {h})} ) by ;
end;
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: ( not s in {(Pb \/ {h})} or s in PARTITIONS X )
assume s in {(Pb \/ {h})} ; :: thesis:
then s = Pb \/ {h} by TARSKI:def 1;
hence s in PARTITIONS X by ; :: thesis: verum
end;
then C \/ {(Pb \/ {h})} c= PARTITIONS X by XBOOLE_1:8;
then C \/ {(Pb \/ {h})} in RL by ;
then C = C \/ {(Pb \/ {h})} by ;
hence h in union C by ; :: thesis: verum
end;
suppose A107: Cb = {} ; :: thesis: h in union C
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 ;
defpred S4[ set ] means \$1 c= hw;
consider PT being set such that
A112: for a being set holds
( a in PT iff ( a in PS & S4[a] ) ) from 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 ;
then Pmin \ {hw} c= H ;
then A115: PT \/ (Pmin \ {hw}) c= H by ;
A116: now :: thesis: for P3 being set st P3 in C \/ {(PT \/ (Pmin \ {hw}))} holds
P3 c= H
let P3 be set ; :: thesis: ( P3 in C \/ {(PT \/ (Pmin \ {hw}))} implies b1 c= H )
assume A117: P3 in C \/ {(PT \/ (Pmin \ {hw}))} ; :: thesis: b1 c= H
per cases ( P3 in C or P3 in {(PT \/ (Pmin \ {hw}))} ) by ;
suppose P3 in C ; :: thesis: b1 c= H
hence P3 c= H by ; :: thesis: verum
end;
suppose P3 in {(PT \/ (Pmin \ {hw}))} ; :: thesis: b1 c= H
hence P3 c= H by ; :: thesis: verum
end;
end;
end;
Pmin in C by ;
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 ;
then A120: PT \/ (Pmin \ {hw}) is_finer_than Pmin by ;
A121: now :: thesis: for P3 being set holds
( not P3 in C or PT \/ (Pmin \ {hw}) is_finer_than P3 or P3 is_finer_than PT \/ (Pmin \ {hw}) )
let P3 be set ; :: thesis: ( not P3 in C or PT \/ (Pmin \ {hw}) is_finer_than P3 or P3 is_finer_than PT \/ (Pmin \ {hw}) )
assume P3 in C ; :: thesis: ( PT \/ (Pmin \ {hw}) is_finer_than P3 or P3 is_finer_than PT \/ (Pmin \ {hw}) )
then Pmin is_finer_than P3 by ;
hence ( PT \/ (Pmin \ {hw}) is_finer_than P3 or P3 is_finer_than PT \/ (Pmin \ {hw}) ) by ; :: thesis: verum
end;
A122: now :: thesis: for P1, P2 being set st P1 in C \/ {(PT \/ (Pmin \ {hw}))} & P2 in C \/ {(PT \/ (Pmin \ {hw}))} & not P1 is_finer_than P2 holds
P2 is_finer_than P1
let P1, P2 be set ; :: thesis: ( P1 in C \/ {(PT \/ (Pmin \ {hw}))} & P2 in C \/ {(PT \/ (Pmin \ {hw}))} & not b1 is_finer_than b2 implies b2 is_finer_than b1 )
assume that
A123: P1 in C \/ {(PT \/ (Pmin \ {hw}))} and
A124: P2 in C \/ {(PT \/ (Pmin \ {hw}))} ; :: thesis: ( b1 is_finer_than b2 or b2 is_finer_than b1 )
per cases ( P1 in C or P1 in {(PT \/ (Pmin \ {hw}))} ) by ;
suppose P1 in {(PT \/ (Pmin \ {hw}))} ; :: thesis: ( b1 is_finer_than b2 or b2 is_finer_than b1 )
then A128: P1 = PT \/ (Pmin \ {hw}) by TARSKI:def 1;
per cases ( P2 in C or P2 in {(PT \/ (Pmin \ {hw}))} ) by ;
suppose P2 in {(PT \/ (Pmin \ {hw}))} ; :: thesis: ( b1 is_finer_than b2 or b2 is_finer_than b1 )
hence ( P1 is_finer_than P2 or P2 is_finer_than P1 ) by ; :: thesis: verum
end;
end;
end;
end;
end;
A129: PT \/ (Pmin \ {hw}) is a_partition of X by ;
{(PT \/ (Pmin \ {hw}))} c= PARTITIONS X
proof
let s be object ; :: according to TARSKI:def 3 :: thesis: ( not s in {(PT \/ (Pmin \ {hw}))} or s in PARTITIONS X )
assume s in {(PT \/ (Pmin \ {hw}))} ; :: thesis:
then s = PT \/ (Pmin \ {hw}) by TARSKI:def 1;
hence s in PARTITIONS X by ; :: thesis: verum
end;
then C \/ {(PT \/ (Pmin \ {hw}))} c= PARTITIONS X by XBOOLE_1:8;
then C \/ {(PT \/ (Pmin \ {hw}))} in RL by ;
then A130: C = C \/ {(PT \/ (Pmin \ {hw}))} by ;
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 ;
hence h in union C by ; :: thesis: verum
end;
end;
end;
hence h in union C ; :: thesis: verum
end;
end;
end;
take C ; :: thesis: ( C is Classification of X & union C = H )
union C c= H
proof
let h be object ; :: according to TARSKI:def 3 :: thesis: ( not h in union C or h in H )
assume h in union C ; :: thesis: h in H
then consider P being set such that
A134: h in P and
A135: P in C by TARSKI:def 4;
P c= H by ;
hence h in H by A134; :: thesis: verum
end;
hence ( C is Classification of X & union C = H ) by ; :: thesis: verum