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;

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 = {} )
;

end;

suppose A8:
Y <> {}
; :: thesis: B is a_partition of Y

Y c= union B

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: verum

end;proof

then A39:
union B = Y
by XBOOLE_0:def 10;
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 A6, A9, TARSKI:def 4;

defpred S_{1}[ 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_{1}[h] ) )
from XFAMILY:sch 1();

A14: D c= H by A13;

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;

A22: {min9} c= H by A20, TARSKI:def 1;

set C = B \/ {min9};

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

consider D being set such that

A13: for h being set holds

( h in D iff ( h in H & S

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

then A19:
D is c=-linear
by ORDINAL1:def 8;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

hence h1,h2 are_c=-comparable by XBOOLE_0:def 9; :: thesis: verum

end;assume that

A15: h1 in D and

A16: h2 in D ; :: thesis: h1,h2 are_c=-comparable

now :: thesis: not h1 misses h2

then
( h1 c= h2 or h2 c= h1 )
by A7, A14, A15, A16;A17:
x in h2
by A13, A16;

assume A18: h1 misses h2 ; :: thesis: contradiction

x in h1 by A13, A15;

hence contradiction by A18, A17, XBOOLE_0:3; :: thesis: verum

end;assume A18: h1 misses h2 ; :: thesis: contradiction

x in h1 by A13, A15;

hence contradiction by A18, A17, XBOOLE_0:3; :: thesis: verum

hence h1,h2 are_c=-comparable by XBOOLE_0:def 9; :: thesis: verum

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;

A22: {min9} c= H by A20, TARSKI:def 1;

set C = B \/ {min9};

now :: thesis: for b1 being set st b1 in B holds

b1 misses min9

then A36:
for b being set st b 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 A10, A23, TARSKI:def 4;

A25: not b1 c= min9

end;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 A10, A23, TARSKI:def 4;

A25: not b1 c= min9

proof

not min9 c= b1
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: contradiction

then b19 c= k by A29;

hence contradiction by A28, A30, XBOOLE_0:3; :: thesis: verum

end;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: contradiction

then b19 c= k by A29;

hence contradiction by A28, A30, XBOOLE_0:3; :: thesis: verum

proof

hence
b1 misses min9
by A4, A7, A20, A23, A25; :: thesis: verum
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: contradiction

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: verum

end;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: contradiction

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: verum

( 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

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: verum

suppose A40:
Y = {}
; :: thesis: B is a_partition of Y

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

end;