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
A4: 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
A5: for L being set holds
( L in RL iff ( L in bool (PARTITIONS X) & S₁[L] ) ) from XBOOLE_0:sch 1();
union H = X by ABIAN:4;
then consider h being set such that
A6: h in H by XBOOLE_0:def 1, ZFMISC_1:2;
reconsider h = h as Subset of X by A6;
consider PX being a_partition of X such that
h in PX and
A7: PX c= H by A1, A2, A6, Th17;
set L = {PX};
A8: {PX} c= PARTITIONS X

proof

let l be set ; :: according to TARSKI:def 3 :: thesis: ( not l in {PX} or l in PARTITIONS X )
assume A9: l in {PX} ; :: thesis: l in PARTITIONS X
l = PX by A9, TARSKI:def 1;
hence l in PARTITIONS X by PARTIT1:def 3; :: thesis: verum

end;

A10: for a being set st a in {PX} holds
a c= H by A7, TARSKI:def 1;

now

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 ( P1 in {PX} & P2 in {PX} ) ; :: thesis: ( P1 is_finer_than P2 or P2 is_finer_than P1 )
then ( P1 = PX & P2 = PX ) by TARSKI:def 1;
hence ( P1 is_finer_than P2 or P2 is_finer_than P1 ) ; :: thesis: verum

end;

then A11: {PX} in RL by A5, A8, A10;

now

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
A12: Z c= RL and
A13: 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 ) )

A14: now

let X1, X2 be set ; :: thesis: ( X1 in Z & X2 in Z & not X1 c= X2 implies X2 c= X1 )
assume ( X1 in Z & X2 in Z ) ; :: thesis: ( X1 c= X2 or X2 c= X1 )
then X1,X2 are_c=-comparable by A13, ORDINAL1:def 9;
hence ( X1 c= X2 or X2 c= X1 ) by XBOOLE_0:def 9; :: thesis: verum

end;

set Y = union Z;
take Y = union Z; :: thesis: ( Y in RL & ( for X1 being set st X1 in Z holds
X1 c= Y ) )
A15: Y c= PARTITIONS X

proof

let P be set ; :: according to TARSKI:def 3 :: thesis: ( not P in Y or P in PARTITIONS X )
assume A16: P in Y ; :: thesis: P in PARTITIONS X
consider L4 being set such that
A17: ( P in L4 & L4 in Z ) by A16, TARSKI:def 4;
L4 in bool (PARTITIONS X) by A5, A12, A17;
hence P in PARTITIONS X by A17; :: thesis: verum

end;

A18: now

let P be set ; :: thesis: ( P in Y implies P c= H )
assume P in Y ; :: thesis: P c= H
then consider L3 being set such that
A19: ( P in L3 & L3 in Z ) by TARSKI:def 4;
thus P c= H by A5, A12, A19; :: thesis: verum

end;

now

let P1, P2 be set ; :: thesis: ( P1 in Y & P2 in Y & not b₁ is_finer_than b₂ implies b₂ is_finer_than b₁ )
assume A20: ( P1 in Y & P2 in Y ) ; :: thesis: ( b₁ is_finer_than b₂ or b₂ is_finer_than b₁ )
then consider L1 being set such that
A21: ( P1 in L1 & L1 in Z ) by TARSKI:def 4;
consider L2 being set such that
A22: ( P2 in L2 & L2 in Z ) by A20, TARSKI:def 4;

per cases ( L1 c= L2 or L2 c= L1 ) by A14, A21, A22;

suppose L1 c= L2 ; :: thesis: ( b₁ is_finer_than b₂ or b₂ is_finer_than b₁ )

hence ( P1 is_finer_than P2 or P2 is_finer_than P1 ) by A5, A12, A21, A22; :: thesis: verum

end;

suppose L2 c= L1 ; :: thesis: ( b₁ is_finer_than b₂ or b₂ is_finer_than b₁ )

hence ( P1 is_finer_than P2 or P2 is_finer_than P1 ) by A5, A12, A21, A22; :: thesis: verum

end;

end;

end;

hence Y in RL by A5, A15, A18; :: 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:92; :: thesis: verum

end;

then consider C being set such that
A23: C in RL and
A24: for Z being set st Z in RL & Z <> C holds
not C c= Z by A11, ORDERS_1:175;
reconsider C = C as Subset of (PARTITIONS X) by A5, A23;
take C ; :: thesis: ( C is Classification of X & union C = H )
A25: 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
A26: P1 in C and
A27: 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 A5, A23, A26, A27; :: thesis: verum

end;

A28: C <> {} by A11, A24, XBOOLE_1:2;
union C = H

proof

thus union C c= H :: according to XBOOLE_0:def 10 :: thesis: H c= union C

proof

let h be set ; :: according to TARSKI:def 3 :: thesis: ( not h in union C or h in H )
assume A29: h in union C ; :: thesis: h in H
consider P being set such that
A30: ( h in P & P in C ) by A29, TARSKI:def 4;
P c= H by A5, A23, A30;
hence h in H by A30; :: thesis: verum

end;

thus H c= union C :: thesis: verum

proof

let h be set ; :: according to TARSKI:def 3 :: thesis: ( not h in H or h in union C )
assume A31: h in H ; :: thesis: h in union C

per cases ( not h in union C or h in union C ) ;

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

consider PS being a_partition of X such that
A33: h in PS and
A34: PS c= H by A1, A2, A31, Th17;
A35: h <> {} by A33, EQREL_1:def 6;
defpred S₂[ set ] means ex hx being set st
( hx in $1 & h c= hx & h <> hx );
consider Ca being set such that
A36: for p being set holds
( p in Ca iff ( p in C & S₂[p] ) ) from XBOOLE_0:sch 1();
A37: Ca c= C

proof

let s be set ; :: according to TARSKI:def 3 :: thesis: ( not s in Ca or s in C )
assume A38: s in Ca ; :: thesis: s in C
thus s in C by A36, A38; :: thesis: verum

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();
A40: Cb c= C

proof

let s be set ; :: according to TARSKI:def 3 :: thesis: ( not s in Cb or s in C )
assume A41: s in Cb ; :: thesis: s in C
thus s in C by A39, A41; :: thesis: verum

end;

A42: now

let p be set ; :: thesis: ( p in C implies ex hv being set st
( hv in p & not hv misses h ) )
assume A43: p in C ; :: thesis: ex hv being set st
( hv in p & not hv misses h )
assume A44: for hv being set st hv in p holds
hv misses h ; :: thesis: contradiction
consider t being set such that
A45: t in h by A35, XBOOLE_0:def 1;
p is a_partition of X by A43, PARTIT1:def 3;
then union p = X by EQREL_1:def 6;
then consider v being set such that
A46: ( t in v & v in p ) by A31, A45, TARSKI:def 4;
not v misses h by A45, A46, XBOOLE_0:3;
hence contradiction by A44, A46; :: thesis: verum

end;

A47: C = Ca \/ Cb

proof

thus C c= Ca \/ Cb :: according to XBOOLE_0:def 10 :: thesis: Ca \/ Cb c= C

proof

let p be set ; :: according to TARSKI:def 3 :: thesis: ( not p in C or p in Ca \/ Cb )
assume A48: p in C ; :: thesis: p in Ca \/ Cb
consider hv being set such that
A49: ( hv in p & not hv misses h ) by A42, A48;
A50: p c= H by A5, A23, A48;
A51: h <> hv by A32, A48, A49, TARSKI:def 4;

per cases ( hv c= h or h c= hv ) by A4, A31, A49, A50, Def3;

suppose hv c= h ; :: thesis: p in Ca \/ Cb

then p in Cb by A39, A48, A49, A51;
hence p in Ca \/ Cb by XBOOLE_0:def 3; :: thesis: verum

end;

suppose h c= hv ; :: thesis: p in Ca \/ Cb

then p in Ca by A36, A48, A49, A51;
hence p in Ca \/ Cb by XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

thus Ca \/ Cb c= C by A37, A40, XBOOLE_1:8; :: thesis: verum

end;

then A52: Ca c= C by XBOOLE_1:7;
A53: Cb c= C by A47, XBOOLE_1:7;
A54: Ca c= PARTITIONS X by A52, XBOOLE_1:1;

A55: now

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 A56: ( P1 in Ca & P2 in Ca ) ; :: thesis: ( P1 is_finer_than P2 or P2 is_finer_than P1 )
( P1 in C & P2 in C ) by A52, A56;
then ( P1 is a_partition of X & P2 is a_partition of X ) by PARTIT1:def 3;
hence ( P1 is_finer_than P2 or P2 is_finer_than P1 ) by A25, A52, A56, TAXONOM1:def 1; :: thesis: verum

end;

A57: Cb c= PARTITIONS X by A53, XBOOLE_1:1;

A58: now

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 A59: ( P1 in Cb & P2 in Cb ) ; :: thesis: ( P1 is_finer_than P2 or P2 is_finer_than P1 )
( P1 in C & P2 in C ) by A53, A59;
then ( P1 is a_partition of X & P2 is a_partition of X ) by PARTIT1:def 3;
hence ( P1 is_finer_than P2 or P2 is_finer_than P1 ) by A25, A53, A59, TAXONOM1:def 1; :: thesis: verum

end;

now

per cases ( Cb <> {} or Cb = {} ) ;

suppose Cb <> {} ; :: thesis: h in union C

then consider PX, Pmax being set such that
A60: ( PX in Cb & Pmax in Cb ) and
A61: for PZ being set st PZ in Cb holds
( PZ is_finer_than Pmax & PX is_finer_than PZ ) by A3, A57, A58;
A62: Pmax c= H by A5, A23, A53, A60;
Pmax in C by A53, A60;
then A63: Pmax is a_partition of X by PARTIT1:def 3;
defpred S₄[ set ] means $1 misses h;
consider Pb being set such that
A64: for x being set holds
( x in Pb iff ( x in Pmax & S₄[x] ) ) from XBOOLE_0:sch 1();
set PS1 = Pb \/ {h};
Pb c= Pmax

proof

let s be set ; :: according to TARSKI:def 3 :: thesis: ( not s in Pb or s in Pmax )
assume s in Pb ; :: thesis: s in Pmax
hence s in Pmax by A64; :: thesis: verum

end;

then A65: Pb c= H by A62, XBOOLE_1:1;
A66: for a being set holds
( not a in Pmax or a c= h or h c= a or h misses a ) by A4, A31, A62, Def3;
A67: ex hx being set st
( hx in Pmax & hx c= h & h <> hx ) by A39, A60;
then A68: Pb \/ {h} is a_partition of X by A31, A35, A63, A64, A66, Th19;
A69: {(Pb \/ {h})} c= PARTITIONS X

proof

let s be set ; :: according to TARSKI:def 3 :: thesis: ( not s in {(Pb \/ {h})} or s in PARTITIONS X )
assume A70: s in {(Pb \/ {h})} ; :: thesis: s in PARTITIONS X
s = Pb \/ {h} by A70, TARSKI:def 1;
hence s in PARTITIONS X by A68, PARTIT1:def 3; :: thesis: verum

end;

A71: {h} c= H

proof

let s be set ; :: according to TARSKI:def 3 :: thesis: ( not s in {h} or s in H )
assume A72: s in {h} ; :: thesis: s in H
thus s in H by A31, A72, TARSKI:def 1; :: thesis: verum

end;

h in {h} by TARSKI:def 1;
then A73: h in Pb \/ {h} by XBOOLE_0:def 3;
A74: Pb \/ {h} c= H by A65, A71, XBOOLE_1:8;
set C1 = C \/ {(Pb \/ {h})};
Pb \/ {h} in {(Pb \/ {h})} by TARSKI:def 1;
then A75: Pb \/ {h} in C \/ {(Pb \/ {h})} by XBOOLE_0:def 3;
A76: C \/ {(Pb \/ {h})} c= PARTITIONS X by A69, XBOOLE_1:8;

A77: now

let P3 be set ; :: thesis: ( P3 in C \/ {(Pb \/ {h})} implies b₁ c= H )
assume A78: P3 in C \/ {(Pb \/ {h})} ; :: thesis: b₁ c= H

per cases ( P3 in C or P3 in {(Pb \/ {h})} ) by A78, XBOOLE_0:def 3;

suppose P3 in C ; :: thesis: b₁ c= H

hence P3 c= H by A5, A23; :: thesis: verum

end;

suppose P3 in {(Pb \/ {h})} ; :: thesis: b₁ c= H

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

end;

end;

end;

A79: Pmax is_finer_than Pb \/ {h} by A31, A35, A63, A64, A66, A67, Th19;

A80: now

let P3 be set ; :: thesis: ( not P3 in C or Pb \/ {h} is_finer_than b₁ or b₁ is_finer_than Pb \/ {h} )
assume A81: P3 in C ; :: thesis: ( Pb \/ {h} is_finer_than b₁ or b₁ is_finer_than Pb \/ {h} )

per cases ( Ca = {} or Ca <> {} ) ;

suppose Ca = {} ; :: thesis: ( Pb \/ {h} is_finer_than b₁ or b₁ is_finer_than Pb \/ {h} )

then P3 is_finer_than Pmax by A47, A61, A81;
hence ( Pb \/ {h} is_finer_than P3 or P3 is_finer_than Pb \/ {h} ) by A79, SETFAM_1:23; :: thesis: verum

end;

suppose A82: Ca <> {} ; :: thesis: ( Pb \/ {h} is_finer_than b₁ or b₁ is_finer_than Pb \/ {h} )

now

per cases ( P3 in Ca or P3 in Cb ) by A47, A81, XBOOLE_0:def 3;

suppose A83: P3 in Ca ; :: thesis: ( Pb \/ {h} is_finer_than P3 or P3 is_finer_than Pb \/ {h} )

consider Pmin, PY being set such that
A84: ( Pmin in Ca & 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, A54, A55, A82;
Pmin in C by A52, A84;
then A86: Pmin is a_partition of X by PARTIT1:def 3;
consider hw being set such that
A87: ( hw in Pmin & h c= hw & h <> hw ) by A36, A84;
Pmax is_finer_than Pmin

proof

A88: ( Pmin in C & Pmax in C ) by A47, A60, A84, XBOOLE_0:def 3;
then A89: ( Pmin is a_partition of X & Pmax is a_partition of X ) by PARTIT1:def 3;

now

assume A90: Pmin is_finer_than Pmax ; :: thesis: contradiction
consider hx being set such that
A91: ( hx in Pmin & h c= hx & h <> hx ) by A36, A84;
consider hy being set such that
A92: ( hy in Pmax & hy c= h & h <> hy ) by A39, A60;
A93: hy c= hx by A91, A92, XBOOLE_1:1;
consider hz being set such that
A94: ( hz in Pmax & hx c= hz ) by A90, A91, SETFAM_1:def 2;
not hy is empty by A63, A92, EQREL_1:def 6;
then hy meets hz by A93, A94, Lm4, XBOOLE_1:1;
then hy = hz by A63, A92, A94, EQREL_1:def 6;
then hx c= h by A92, A94, XBOOLE_1:1;
hence contradiction by A91, XBOOLE_0:def 10; :: thesis: verum

end;

hence Pmax is_finer_than Pmin by A25, A88, A89, TAXONOM1:def 1; :: thesis: verum

end;

then A95: Pb \/ {h} is_finer_than Pmin by A31, A35, A63, A64, A66, A67, A86, A87, Th19;
Pmin is_finer_than P3 by A83, A85;
hence ( Pb \/ {h} is_finer_than P3 or P3 is_finer_than Pb \/ {h} ) by A95, SETFAM_1:23; :: thesis: verum

end;

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

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

end;

end;

end;

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

end;

end;

end;

now

let P1, P2 be set ; :: thesis: ( P1 in C \/ {(Pb \/ {h})} & P2 in C \/ {(Pb \/ {h})} & not b₁ is_finer_than b₂ implies b₂ is_finer_than b₁ )
assume A96: ( P1 in C \/ {(Pb \/ {h})} & P2 in C \/ {(Pb \/ {h})} ) ; :: thesis: ( b₁ is_finer_than b₂ or b₂ is_finer_than b₁ )

per cases ( P1 in C or P1 in {(Pb \/ {h})} ) by A96, XBOOLE_0:def 3;

suppose A97: P1 in C ; :: thesis: ( b₁ is_finer_than b₂ or b₂ is_finer_than b₁ )

per cases ( P2 in C or P2 in {(Pb \/ {h})} ) by A96, XBOOLE_0:def 3;

suppose A98: P2 in C ; :: thesis: ( b₁ is_finer_than b₂ or b₂ is_finer_than b₁ )

A99: P1 is a_partition of X by A97, PARTIT1:def 3;
P2 is a_partition of X by A98, PARTIT1:def 3;
hence ( P1 is_finer_than P2 or P2 is_finer_than P1 ) by A25, A97, A98, A99, TAXONOM1:def 1; :: thesis: verum

end;

suppose P2 in {(Pb \/ {h})} ; :: thesis: ( b₁ is_finer_than b₂ or b₂ is_finer_than b₁ )

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

end;

end;

end;

suppose P1 in {(Pb \/ {h})} ; :: thesis: ( b₁ is_finer_than b₂ or b₂ is_finer_than b₁ )

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

per cases ( P2 in C or P2 in {(Pb \/ {h})} ) by A96, XBOOLE_0:def 3;

suppose P2 in C ; :: thesis: ( b₁ is_finer_than b₂ or b₂ is_finer_than b₁ )

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

end;

suppose P2 in {(Pb \/ {h})} ; :: thesis: ( b₁ is_finer_than b₂ or b₂ is_finer_than b₁ )

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

end;

end;

end;

end;

end;

then C \/ {(Pb \/ {h})} in RL by A5, A76, A77;
then C = C \/ {(Pb \/ {h})} by A24, XBOOLE_1:7;
hence h in union C by A73, A75, TARSKI:def 4; :: thesis: verum

end;

suppose A101: Cb = {} ; :: thesis: h in union C

then consider Pmin, PY being set such that
A102: ( Pmin in Ca & PY in Ca ) and
A103: for PZ being set st PZ in Ca holds
( PZ is_finer_than PY & Pmin is_finer_than PZ ) by A3, A28, A47, A55;
A104: Pmin c= H by A5, A23, A52, A102;
Pmin in C by A52, A102;
then A105: Pmin is a_partition of X by PARTIT1:def 3;
consider hw being set such that
A106: ( hw in Pmin & h c= hw & h <> hw ) by A36, A102;
A107: Pmin \ {hw} c= H by A104, XBOOLE_1:1;
defpred S₄[ set ] means $1 c= hw;
consider PT being set such that
A108: for a being set holds
( a in PT iff ( a in PS & S₄[a] ) ) from XBOOLE_0:sch 1();
set PS1 = PT \/ (Pmin \ {hw});
A109: PT c= PT \/ (Pmin \ {hw}) by XBOOLE_1:7;
A110: h in PT by A33, A106, A108;
PT c= PS

proof

let s be set ; :: according to TARSKI:def 3 :: thesis: ( not s in PT or s in PS )
assume s in PT ; :: thesis: s in PS
hence s in PS by A108; :: thesis: verum

end;

then PT c= H by A34, XBOOLE_1:1;
then A111: PT \/ (Pmin \ {hw}) c= H by A107, XBOOLE_1:8;
A112: for a being set holds
( not a in PS or a c= hw or hw c= a or hw misses a ) by A4, A34, A104, A106, Def3;
then A113: PT \/ (Pmin \ {hw}) is a_partition of X by A33, A35, A105, A106, A108, Th18;
A114: {(PT \/ (Pmin \ {hw}))} c= PARTITIONS X

proof

let s be set ; :: according to TARSKI:def 3 :: thesis: ( not s in {(PT \/ (Pmin \ {hw}))} or s in PARTITIONS X )
assume A115: s in {(PT \/ (Pmin \ {hw}))} ; :: thesis: s in PARTITIONS X
s = PT \/ (Pmin \ {hw}) by A115, TARSKI:def 1;
hence s in PARTITIONS X by A113, PARTIT1:def 3; :: thesis: verum

end;

set C1 = C \/ {(PT \/ (Pmin \ {hw}))};
A116: {(PT \/ (Pmin \ {hw}))} c= C \/ {(PT \/ (Pmin \ {hw}))} by XBOOLE_1:7;
A117: PT \/ (Pmin \ {hw}) in {(PT \/ (Pmin \ {hw}))} by TARSKI:def 1;
A118: PT \/ (Pmin \ {hw}) is_finer_than Pmin by A33, A35, A105, A106, A108, A112, Th18;
A119: C \/ {(PT \/ (Pmin \ {hw}))} c= PARTITIONS X by A114, XBOOLE_1:8;

A120: now

let P3 be set ; :: thesis: ( P3 in C \/ {(PT \/ (Pmin \ {hw}))} implies b₁ c= H )
assume A121: P3 in C \/ {(PT \/ (Pmin \ {hw}))} ; :: thesis: b₁ c= H

per cases ( P3 in C or P3 in {(PT \/ (Pmin \ {hw}))} ) by A121, XBOOLE_0:def 3;

suppose P3 in C ; :: thesis: b₁ c= H

hence P3 c= H by A5, A23; :: thesis: verum

end;

suppose P3 in {(PT \/ (Pmin \ {hw}))} ; :: thesis: b₁ c= H

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

end;

end;

end;

A122: now

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 A123: P3 in C ; :: thesis: ( PT \/ (Pmin \ {hw}) is_finer_than P3 or P3 is_finer_than PT \/ (Pmin \ {hw}) )
Pmin is_finer_than P3 by A47, A101, A103, A123;
hence ( PT \/ (Pmin \ {hw}) is_finer_than P3 or P3 is_finer_than PT \/ (Pmin \ {hw}) ) by A118, SETFAM_1:23; :: thesis: verum

end;

now

let P1, P2 be set ; :: thesis: ( P1 in C \/ {(PT \/ (Pmin \ {hw}))} & P2 in C \/ {(PT \/ (Pmin \ {hw}))} & not b₁ is_finer_than b₂ implies b₂ is_finer_than b₁ )
assume A124: ( P1 in C \/ {(PT \/ (Pmin \ {hw}))} & P2 in C \/ {(PT \/ (Pmin \ {hw}))} ) ; :: thesis: ( b₁ is_finer_than b₂ or b₂ is_finer_than b₁ )

per cases ( P1 in C or P1 in {(PT \/ (Pmin \ {hw}))} ) by A124, XBOOLE_0:def 3;

suppose A125: P1 in C ; :: thesis: ( b₁ is_finer_than b₂ or b₂ is_finer_than b₁ )

per cases ( P2 in C or P2 in {(PT \/ (Pmin \ {hw}))} ) by A124, XBOOLE_0:def 3;

suppose A126: P2 in C ; :: thesis: ( b₁ is_finer_than b₂ or b₂ is_finer_than b₁ )

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

end;

suppose P2 in {(PT \/ (Pmin \ {hw}))} ; :: thesis: ( b₁ is_finer_than b₂ or b₂ is_finer_than b₁ )

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

end;

end;

end;

suppose P1 in {(PT \/ (Pmin \ {hw}))} ; :: thesis: ( b₁ is_finer_than b₂ or b₂ is_finer_than b₁ )

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

per cases ( P2 in C or P2 in {(PT \/ (Pmin \ {hw}))} ) by A124, XBOOLE_0:def 3;

suppose P2 in C ; :: thesis: ( b₁ is_finer_than b₂ or b₂ is_finer_than b₁ )

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

end;

suppose P2 in {(PT \/ (Pmin \ {hw}))} ; :: thesis: ( b₁ is_finer_than b₂ or b₂ is_finer_than b₁ )

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

end;

end;

end;

end;

end;

then C \/ {(PT \/ (Pmin \ {hw}))} in RL by A5, A119, A120;
then C = C \/ {(PT \/ (Pmin \ {hw}))} by A24, XBOOLE_1:7;
hence h in union C by A109, A110, A116, A117, TARSKI:def 4; :: thesis: verum

end;

end;

end;

hence h in union C ; :: thesis: verum

end;

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

hence h in union C ; :: thesis: verum

end;

end;

end;

end;

hence ( C is Classification of X & union C = H ) by A25; :: thesis: verum