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
for B being mutually-disjoint Subset-Family of Y st A in B & B c= H & ( for C being mutually-disjoint Subset-Family of Y st A in C & C c= H & B c= C holds
B = C ) holds
B is a_partition of Y

let H be covering T_3 Hierarchy of Y; :: thesis: ( H is lower-bounded & not {} in H implies for A being Subset of Y
for B being mutually-disjoint Subset-Family of Y st A in B & B c= H & ( for C being mutually-disjoint Subset-Family of Y st A in C & C c= H & B c= C holds
B = C ) holds
B is a_partition of Y )

assume that
A1: H is lower-bounded and
A2: not {} in H ; :: thesis: for A being Subset of Y
for B being mutually-disjoint Subset-Family of Y st A in B & B c= H & ( for C being mutually-disjoint Subset-Family of Y st A in C & C c= H & B c= C holds
B = C ) holds
B is a_partition of Y

let A be Subset of Y; :: thesis: for B being mutually-disjoint Subset-Family of Y st A in B & B c= H & ( for C being mutually-disjoint Subset-Family of Y st A in C & C c= H & B c= C holds
B = C ) holds
B is a_partition of Y

let B be mutually-disjoint Subset-Family of Y; :: thesis: ( A in B & B c= H & ( for C being mutually-disjoint Subset-Family of Y st A in C & C c= H & B c= C holds
B = C ) implies B is a_partition of Y )

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 & B c= C holds
B = C ; :: thesis: B is a_partition of Y
A6: union H = Y by ABIAN:4;
A7: H is hierarchic by Def4;
per cases ( Y <> {} or Y = {} ) ;
suppose A8: Y <> {} ; :: thesis: B is a_partition of Y
Y c= union B
proof
assume not Y c= union B ; :: thesis: contradiction
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 ;
defpred S1[ set ] means x in \$1;
consider D being set such that
A13: for h being set holds
( h in D iff ( h in H & S1[h] ) ) from A14: D c= H by A13;
now :: thesis: for h1, h2 being set st h1 in D & h2 in D holds
h1,h2 are_c=-comparable
let h1, h2 be set ; :: thesis: ( h1 in D & h2 in D implies h1,h2 are_c=-comparable )
assume that
A15: h1 in D and
A16: h2 in D ; :: thesis: h1,h2 are_c=-comparable
now :: thesis: not h1 misses h2
A17: x in h2 by ;
assume A18: h1 misses h2 ; :: thesis: contradiction
x in h1 by ;
hence contradiction by A18, A17, XBOOLE_0:3; :: thesis: verum
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: verum
end;
then A19: D is c=-linear by ORDINAL1:def 8;
xx in D by ;
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;
A22: {min9} c= H by ;
set C = B \/ {min9};
now :: thesis: for b1 being set st b1 in B holds
b1 misses min9
reconsider x9 = x as Element of Y by A9;
let b1 be set ; :: thesis: ( b1 in B implies b1 misses min9 )
assume A23: b1 in B ; :: thesis: b1 misses min9
reconsider b19 = b1 as Subset of Y by A23;
A24: not x9 in b19 by ;
A25: not b1 c= min9
proof
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 ;
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: contradiction
then b19 c= k by A29;
hence contradiction by A28, A30, XBOOLE_0:3; :: thesis: verum
end;
not min9 c= b1
proof
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 ;
then meet D c= k by SETFAM_1:3;
then A34: min9 c= k by A21;
assume A35: min9 c= b1 ; :: thesis: contradiction
ex y being object st y in min9 by ;
hence contradiction by A35, A33, A34, XBOOLE_0:3; :: thesis: verum
end;
hence b1 misses min9 by A4, A7, A20, A23, A25; :: thesis: verum
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;
A38: B c= B \/ {min9} by XBOOLE_1:7;
union (B \/ {min9}) <> union B by A2, A20, A36, Th11;
hence contradiction by A3, A4, A5, A37, A22, A38, XBOOLE_1:8; :: thesis: verum
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 ; :: thesis: verum
end;
suppose A40: Y = {} ; :: thesis: B is a_partition of Y
end;
end;