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

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

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

let h1, h2 be set ; :: thesis:
assume that
A15: h1 in D and
A16: h2 in D ; :: thesis:

A17: x in h2 by A13, A16;
assume A18: h1 misses h2 ; :: thesis:
x in h1 by A13, A15;
hence contradiction by A18, A17, XBOOLE_0:3; :: thesis:

end;

then ( h1 c= h2 or h2 c= h1 ) by A7, A14, A15, A16;
hence h1,h2 are_c=-comparable by XBOOLE_0:def 9; :: thesis:

end;

then A19: D is c=-linear by ORDINAL1:def 8;
xx in D by A13, A11, A12;
then consider min1 being set such that
A20: min1 in H and
A21: min1 c= meet D by A1, A14, A19;
reconsider min9 = min1 as Subset of Y by A20;
set C = B \/ {min9};
A22: B c= B \/ {min9} by XBOOLE_1:7;

reconsider x9 = x as Element of Y by A9;
let b1 be set ; :: thesis:
assume A23: b1 in B ; :: thesis:
reconsider b19 = b1 as Subset of Y by A23;
A24: not x9 in b19 by A10, A23, TARSKI:def 4;
A25: not b1 c= min9

reconsider b19 = b1 as Subset of Y by A23;
consider k being Subset of Y such that
A26: x9 in k and
A27: k in H and
A28: k misses b19 by A4, A23, A24, Def6;
k in D by A13, A26, A27;
then meet D c= k by SETFAM_1:3;
then A29: min9 c= k by A21;
b1 <> {} by A2, A4, A23;
then A30: ex y being object st y in b19 by XBOOLE_0:def 1;
assume b1 c= min9 ; :: thesis:
then b19 c= k by A29;
hence contradiction by A28, A30, XBOOLE_0:3; :: thesis:

end;

consider k being Subset of Y such that
A31: x9 in k and
A32: k in H and
A33: k misses b19 by A4, A23, A24, Def6;
k in D by A13, A31, A32;
then meet D c= k by SETFAM_1:3;
then A34: min9 c= k by A21;
assume A35: min9 c= b1 ; :: thesis:
ex y being object st y in min9 by A2, A20, XBOOLE_0:def 1;
hence contradiction by A35, A33, A34, XBOOLE_0:3; :: thesis:

end;

hence b1 misses min9 by A4, A7, A20, A23, A25; :: thesis:

end;

then A36: for b being set st b in B holds
( min9 misses b & Y <> {} ) by A8;
then A37: B \/ {min9} is mutually-disjoint Subset-Family of Y by Th11;
{min9} c= H by A20, TARSKI:def 1;
then A38: B \/ {min9} c= H by A4, XBOOLE_1:8;
union (B \/ {min9}) <> union B by A2, A20, A36, Th11;
hence contradiction by A3, A5, A37, A38, A22, ZFMISC_1:77; :: 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 A2, A4, Def5;
hence B is a_partition of Y by A39, EQREL_1:def 4; :: thesis:

end;

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

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

suppose H = {} ; :: thesis:

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

end;

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

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

end;

hence B = {} by A4, A41, ZFMISC_1:33; :: thesis:

end;

end;

end;

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

end;

end;