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:
assume A3: A in H ; :: thesis:
defpred S₁[ set ] means ( A in $1 & $1 is mutually-disjoint & $1 c= H );
consider K being set such that
A4: for S being set holds
( S in K iff ( S in bool (bool Y) & S₁[S] ) ) from XBOOLE_0:sch 1();
set k1 = {A};
A5: A in {A} by TARSKI:def 1;
A6: {A} is mutually-disjoint by Th10;
A7: {A} c= H by A3, ZFMISC_1:37;
{A} c= bool Y by ZFMISC_1:37;
then A8: {A} in K by A4, A5, A6, A7;
for Z being set st Z c= K & Z is c=-linear holds
ex X3 being set st
( X3 in K & ( for X1 being set st X1 in Z holds
X1 c= X3 ) )

let Z be set ; :: thesis:
assume that
A9: Z c= K and
A10: Z is c=-linear ; :: thesis:

A11: now

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

end;

per cases ;

suppose A12: Z <> {} ; :: thesis:

set X3 = union Z;
take union Z ; :: thesis:

consider z being set such that
A13: z in Z by A12, XBOOLE_0:def 1;
A in z by A4, A9, A13;
hence A in union Z by A13, TARSKI:def 4; :: thesis:
A14: for a being set st a in Z holds
a c= H by A4, A9;
then union Z c= H by ZFMISC_1:94;
then union Z c= bool Y by XBOOLE_1:1;
hence union Z in bool (bool Y) ; :: thesis:
thus union Z is mutually-disjoint :: thesis:

let t1, t2 be set ; :: according to TAXONOM2:def 5 :: thesis:
assume that
A15: t1 in union Z and
A16: t2 in union Z and
A17: t1 <> t2 ; :: thesis:
consider v1 being set such that
A18: ( t1 in v1 & v1 in Z ) by A15, TARSKI:def 4;
consider v2 being set such that
A19: ( t2 in v2 & v2 in Z ) by A16, TARSKI:def 4;
A20: v1 is mutually-disjoint by A4, A9, A18;
A21: v2 is mutually-disjoint by A4, A9, A19;

per cases by A11, A18, A19;

suppose v1 c= v2 ; :: thesis:

hence t1 misses t2 by A17, A18, A19, A21, Def5; :: thesis:

end;

suppose v2 c= v1 ; :: thesis:

hence t1 misses t2 by A17, A18, A19, A20, Def5; :: thesis:

end;

thus union Z c= H by A14, ZFMISC_1:94; :: thesis:

end;

hence union Z in K by A4; :: thesis:
thus for X1 being set st X1 in Z holds
X1 c= union Z by ZFMISC_1:92; :: thesis:

end;

suppose A22: Z = {} ; :: thesis:

consider a being set such that
A23: a in K by A8;
take a ; :: thesis:
thus a in K by A23; :: thesis:
thus for X1 being set st X1 in Z holds
X1 c= a by A22; :: thesis:

end;

then consider M being set such that
A24: M in K and
A25: for Z being set st Z in K & Z <> M holds
not M c= Z by A8, ORDERS_1:175;
A26: M c= H by A4, A24;
A27: M is mutually-disjoint Subset-Family of Y by A4, A24;
A28: A in M by A4, A24;

A29: now

let C be mutually-disjoint Subset-Family of Y; :: thesis:
assume A30: ( A in C & C c= H & M c= C ) ; :: thesis:
C in K by A4, A30;
hence M = C by A25, A30; :: thesis:

end;

take M ; :: thesis:
thus ( M is Element of bool (bool Y) & M is a_partition of Y & A in M & M c= H ) by A1, A2, A26, A27, A28, A29, Th16; :: thesis: