let Y be set ; :: thesis: for H being covering T_3 Hierarchy of Y st H is lower-bounded & not {} in H holds

for A being Subset of Y st A in H holds

ex P being a_partition of Y st

( A in P & P c= H )

let H be covering T_3 Hierarchy of Y; :: thesis: ( H is lower-bounded & not {} in H implies for A being Subset of Y st A in H holds

ex P being a_partition of Y st

( A in P & P c= H ) )

assume that

A1: H is lower-bounded and

A2: not {} in H ; :: thesis: for A being Subset of Y st A in H holds

ex P being a_partition of Y st

( A in P & P c= H )

let A be Subset of Y; :: thesis: ( A in H implies ex P being a_partition of Y st

( A in P & P c= H ) )

assume A3: A in H ; :: thesis: ex P being a_partition of Y st

( A in P & P c= H )

set k1 = {A};

A4: {A} c= H by A3, ZFMISC_1:31;

A5: A in {A} by TARSKI:def 1;

A6: {A} c= bool Y by ZFMISC_1:31;

defpred S_{1}[ set ] means ( A in $1 & $1 is mutually-disjoint & $1 c= H );

consider K being set such that

A7: for S being set holds

( S in K iff ( S in bool (bool Y) & S_{1}[S] ) )
from XFAMILY:sch 1();

{A} is mutually-disjoint by Th9;

then A8: {A} in K by A7, A5, A4, A6;

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 ) )

A26: M in K and

A27: for Z being set st Z in K & Z <> M holds

not M c= Z by A8, ORDERS_1:65;

A28: M is mutually-disjoint Subset-Family of Y by A7, A26;

A29: for C being mutually-disjoint Subset-Family of Y st A in C & C c= H & M c= C holds

M = C by A27, A7;

A30: A in M by A7, A26;

take M ; :: thesis: ( M is Element of bool (bool Y) & M is a_partition of Y & A in M & M c= H )

M c= H by A7, A26;

hence ( M is Element of bool (bool Y) & M is a_partition of Y & A in M & M c= H ) by A1, A2, A28, A30, A29, Th15; :: thesis: verum

for A being Subset of Y st A in H holds

ex P being a_partition of Y st

( A in P & P c= H )

let H be covering T_3 Hierarchy of Y; :: thesis: ( H is lower-bounded & not {} in H implies for A being Subset of Y st A in H holds

ex P being a_partition of Y st

( A in P & P c= H ) )

assume that

A1: H is lower-bounded and

A2: not {} in H ; :: thesis: for A being Subset of Y st A in H holds

ex P being a_partition of Y st

( A in P & P c= H )

let A be Subset of Y; :: thesis: ( A in H implies ex P being a_partition of Y st

( A in P & P c= H ) )

assume A3: A in H ; :: thesis: ex P being a_partition of Y st

( A in P & P c= H )

set k1 = {A};

A4: {A} c= H by A3, ZFMISC_1:31;

A5: A in {A} by TARSKI:def 1;

A6: {A} c= bool Y by ZFMISC_1:31;

defpred S

consider K being set such that

A7: for S being set holds

( S in K iff ( S in bool (bool Y) & S

{A} is mutually-disjoint by Th9;

then A8: {A} in K by A7, A5, A4, A6;

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 ) )

proof

then consider M being set such that
let Z be set ; :: thesis: ( Z c= K & Z is c=-linear implies ex X3 being set st

( X3 in K & ( for X1 being set st X1 in Z holds

X1 c= X3 ) ) )

assume that

A9: Z c= K and

A10: Z is c=-linear ; :: thesis: ex X3 being set st

( X3 in K & ( for X1 being set st X1 in Z holds

X1 c= X3 ) )

A11: for X1, X2 being set st X1 in Z & X2 in Z & not X1 c= X2 holds

X2 c= X1 by XBOOLE_0:def 9, A10, ORDINAL1:def 8;

end;( X3 in K & ( for X1 being set st X1 in Z holds

X1 c= X3 ) ) )

assume that

A9: Z c= K and

A10: Z is c=-linear ; :: thesis: ex X3 being set st

( X3 in K & ( for X1 being set st X1 in Z holds

X1 c= X3 ) )

A11: for X1, X2 being set st X1 in Z & X2 in Z & not X1 c= X2 holds

X2 c= X1 by XBOOLE_0:def 9, A10, ORDINAL1:def 8;

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

end;

suppose A12:
Z <> {}
; :: thesis: ex X3 being set st

( X3 in K & ( for X1 being set st X1 in Z holds

X1 c= X3 ) )

( X3 in K & ( for X1 being set st X1 in Z holds

X1 c= X3 ) )

set X3 = union Z;

take union Z ; :: thesis: ( union Z in K & ( for X1 being set st X1 in Z holds

X1 c= union Z ) )

X1 c= union Z

thus for X1 being set st X1 in Z holds

X1 c= union Z by ZFMISC_1:74; :: thesis: verum

end;take union Z ; :: thesis: ( union Z in K & ( for X1 being set st X1 in Z holds

X1 c= union Z ) )

now :: thesis: ( A in union Z & union Z in bool (bool Y) & union Z is mutually-disjoint & union Z c= H )

hence
union Z in K
by A7; :: thesis: for X1 being set st X1 in Z holds consider z being object such that

A13: z in Z by A12, XBOOLE_0:def 1;

reconsider z = z as set by TARSKI:1;

A in z by A7, A9, A13;

hence A in union Z by A13, TARSKI:def 4; :: thesis: ( union Z in bool (bool Y) & union Z is mutually-disjoint & union Z c= H )

A14: for a being set st a in Z holds

a c= H by A7, A9;

then union Z c= H by ZFMISC_1:76;

then union Z c= bool Y by XBOOLE_1:1;

hence union Z in bool (bool Y) ; :: thesis: ( union Z is mutually-disjoint & union Z c= H )

thus union Z is mutually-disjoint :: thesis: union Z c= H

end;A13: z in Z by A12, XBOOLE_0:def 1;

reconsider z = z as set by TARSKI:1;

A in z by A7, A9, A13;

hence A in union Z by A13, TARSKI:def 4; :: thesis: ( union Z in bool (bool Y) & union Z is mutually-disjoint & union Z c= H )

A14: for a being set st a in Z holds

a c= H by A7, A9;

then union Z c= H by ZFMISC_1:76;

then union Z c= bool Y by XBOOLE_1:1;

hence union Z in bool (bool Y) ; :: thesis: ( union Z is mutually-disjoint & union Z c= H )

thus union Z is mutually-disjoint :: thesis: union Z c= H

proof

thus
union Z c= H
by A14, ZFMISC_1:76; :: thesis: verum
let t1, t2 be set ; :: according to TAXONOM2:def 5 :: thesis: ( t1 in union Z & t2 in union Z & t1 <> t2 implies t1 misses t2 )

assume that

A15: t1 in union Z and

A16: t2 in union Z and

A17: t1 <> t2 ; :: thesis: t1 misses t2

consider v1 being set such that

A18: t1 in v1 and

A19: v1 in Z by A15, TARSKI:def 4;

A20: v1 is mutually-disjoint by A7, A9, A19;

consider v2 being set such that

A21: t2 in v2 and

A22: v2 in Z by A16, TARSKI:def 4;

A23: v2 is mutually-disjoint by A7, A9, A22;

end;assume that

A15: t1 in union Z and

A16: t2 in union Z and

A17: t1 <> t2 ; :: thesis: t1 misses t2

consider v1 being set such that

A18: t1 in v1 and

A19: v1 in Z by A15, TARSKI:def 4;

A20: v1 is mutually-disjoint by A7, A9, A19;

consider v2 being set such that

A21: t2 in v2 and

A22: v2 in Z by A16, TARSKI:def 4;

A23: v2 is mutually-disjoint by A7, A9, A22;

X1 c= union Z

thus for X1 being set st X1 in Z holds

X1 c= union Z by ZFMISC_1:74; :: thesis: verum

suppose A24:
Z = {}
; :: thesis: ex X3 being set st

( X3 in K & ( for X1 being set st X1 in Z holds

X1 c= X3 ) )

( X3 in K & ( for X1 being set st X1 in Z holds

X1 c= X3 ) )

consider a being set such that

A25: a in K by A8;

take a ; :: thesis: ( a in K & ( for X1 being set st X1 in Z holds

X1 c= a ) )

thus a in K by A25; :: thesis: for X1 being set st X1 in Z holds

X1 c= a

thus for X1 being set st X1 in Z holds

X1 c= a by A24; :: thesis: verum

end;A25: a in K by A8;

take a ; :: thesis: ( a in K & ( for X1 being set st X1 in Z holds

X1 c= a ) )

thus a in K by A25; :: thesis: for X1 being set st X1 in Z holds

X1 c= a

thus for X1 being set st X1 in Z holds

X1 c= a by A24; :: thesis: verum

A26: M in K and

A27: for Z being set st Z in K & Z <> M holds

not M c= Z by A8, ORDERS_1:65;

A28: M is mutually-disjoint Subset-Family of Y by A7, A26;

A29: for C being mutually-disjoint Subset-Family of Y st A in C & C c= H & M c= C holds

M = C by A27, A7;

A30: A in M by A7, A26;

take M ; :: thesis: ( M is Element of bool (bool Y) & M is a_partition of Y & A in M & M c= H )

M c= H by A7, A26;

hence ( M is Element of bool (bool Y) & M is a_partition of Y & A in M & M c= H ) by A1, A2, A28, A30, A29, Th15; :: thesis: verum