let Y be set ; :: thesis:
let H be covering T_3 Hierarchy of Y; :: thesis:
assume A1: ( H is lower-bounded & not {} in H ) ; :: thesis:
let A be Subset of Y; :: thesis:
let B be mutually-disjoint Subset-Family of Y; :: thesis:
assume that
A2: A in B and
A3: B c= H and
A4: for C being mutually-disjoint Subset-Family of Y st A in C & C c= H & B c= C holds
B = C ; :: thesis:
A5: union H = Y by ABIAN:4;
A6: H is hierarchic by Def4;

per cases ;

suppose A7: Y <> {} ; :: thesis:

Y c= union B

proof

assume not Y c= union B ; :: thesis:
then consider x being set such that
A8: x in Y and
A9: not x in union B by TARSKI:def 3;
defpred S₁[ set ] means x in $1;
consider D being set such that
A10: for h being set holds
( h in D iff ( h in H & S₁[h] ) ) from XBOOLE_0:sch 1();
consider xx being set such that
A11: ( x in xx & xx in H ) by A5, A8, TARSKI:def 4;
A12: xx in D by A10, A11;
A13: D c= H

proof

let d be set ; :: according to TARSKI:def 3 :: thesis:
assume A14: d in D ; :: thesis:
thus d in H by A10, A14; :: thesis:

end;

now

let h1, h2 be set ; :: thesis:
assume A15: ( h1 in D & h2 in D ) ; :: thesis:

now

assume A16: h1 misses h2 ; :: thesis:
( x in h1 & x in h2 ) by A10, A15;
hence contradiction by A16, XBOOLE_0:3; :: thesis:

end;

then ( h1 c= h2 or h2 c= h1 ) by A6, A13, A15, Def3;
hence h1,h2 are_c=-comparable by XBOOLE_0:def 9; :: thesis:

end;

then D is c=-linear by ORDINAL1:def 9;
then consider min being set such that
A17: min in H and
A18: min c= meet D by A1, A12, A13, Def7;
reconsider min' = min as Subset of Y by A17;

now

let b1 be set ; :: thesis:
assume A19: b1 in B ; :: thesis:
reconsider b1' = b1 as Subset of Y by A19;
reconsider x' = x as Element of Y by A8;
A20: not x' in b1' by A9, A19, TARSKI:def 4;
A21: not min' c= b1

proof

assume A22: min' c= b1 ; :: thesis:
consider k being Subset of Y such that
A23: x' in k and
A24: k in H and
A25: k misses b1' by A3, A19, A20, Def6;
k in D by A10, A23, A24;
then meet D c= k by SETFAM_1:4;
then A26: min' c= k by A18, XBOOLE_1:1;
consider y being set such that
A27: y in min' by A1, A17, XBOOLE_0:def 1;
thus contradiction by A22, A25, A26, A27, XBOOLE_0:3; :: thesis:

end;

not b1 c= min'

proof

assume A28: b1 c= min' ; :: thesis:
reconsider b1' = b1 as Subset of Y by A19;
consider k being Subset of Y such that
A29: x' in k and
A30: k in H and
A31: k misses b1' by A3, A19, A20, Def6;
A32: b1 <> {} by A1, A3, A19;
k in D by A10, A29, A30;
then meet D c= k by SETFAM_1:4;
then min' c= k by A18, XBOOLE_1:1;
then A33: b1' c= k by A28, XBOOLE_1:1;
consider y being set such that
A34: y in b1' by A32, XBOOLE_0:def 1;
thus contradiction by A31, A33, A34, XBOOLE_0:3; :: thesis:

end;

hence b1 misses min' by A3, A6, A17, A19, A21, Def3; :: thesis:

end;

then A35: for b being set st b in B holds
( min' misses b & Y <> {} ) by A7;
set C = B \/ {min'};
A36: ( B \/ {min'} is mutually-disjoint Subset-Family of Y & union (B \/ {min'}) <> union B ) by A1, A17, A35, Th12;
A37: {min'} c= H

proof

let s be set ; :: according to TARSKI:def 3 :: thesis:
assume A38: s in {min'} ; :: thesis:
thus s in H by A17, A38, TARSKI:def 1; :: thesis:

end;

B c= B \/ {min'} by XBOOLE_1:7;
hence contradiction by A2, A3, A4, A36, A37, XBOOLE_1:8; :: thesis:

end;

then A39: union B = Y by XBOOLE_0:def 10;
for A being Subset of Y st A in B holds
( A <> {} & ( for E being Subset of Y holds
( not E in B or A = E or A misses E ) ) ) by A1, A3, Def5;
hence B is a_partition of Y by A39, EQREL_1:def 6; :: thesis:

end;

suppose A40: Y = {} ; :: thesis:

now

per cases by A40, ZFMISC_1:1, ZFMISC_1:39;

suppose H = {} ; :: thesis:

hence B = {} by A3; :: thesis:

end;

suppose A41: H = {{} } ; :: thesis:

B <> {{} }

proof

assume B = {{} } ; :: thesis:
then {} in B by TARSKI:def 1;
hence contradiction by A1, A3; :: thesis:

end;

hence B = {} by A3, A41, ZFMISC_1:39; :: thesis:

end;

hence B is a_partition of Y by A40, EQREL_1:54; :: thesis:

end;