let Y be set ; 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; ( 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
; 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; 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; ( 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
; 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 <> {}
;
B is a_partition of Y
Y c= union B
proof
assume
not
Y c= union B
;
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 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 XFAMILY:sch 1();
A14:
D c= H
by A13;
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;
A22:
{min9} c= H
by A20, TARSKI:def 1;
set C =
B \/ {min9};
now for b1 being set st b1 in B holds
b1 misses min9reconsider x9 =
x as
Element of
Y by A9;
let b1 be
set ;
( b1 in B implies b1 misses min9 )assume A23:
b1 in B
;
b1 misses min9reconsider b19 =
b1 as
Subset of
Y by A23;
A24:
not
x9 in b19
by A10, A23, TARSKI:def 4;
A25:
not
b1 c= min9
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 A13, A31, A32;
then
meet D c= k
by SETFAM_1:3;
then A34:
min9 c= k
by A21;
assume A35:
min9 c= b1
;
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;
verum
end; hence
b1 misses min9
by A4, A7, A20, A23, A25;
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;
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 A39, EQREL_1:def 4;
verum end; end;