let Y be set ; :: thesis: for H being covering Hierarchy of Y

for B being mutually-disjoint Subset-Family of Y st B c= H & ( for C being mutually-disjoint Subset-Family of Y st C c= H & union B c= union C holds

B = C ) holds

B is a_partition of Y

let H be covering Hierarchy of Y; :: thesis: for B being mutually-disjoint Subset-Family of Y st B c= H & ( for C being mutually-disjoint Subset-Family of Y st C c= H & union B c= union C holds

B = C ) holds

B is a_partition of Y

let B be mutually-disjoint Subset-Family of Y; :: thesis: ( B c= H & ( for C being mutually-disjoint Subset-Family of Y st C c= H & union B c= union C holds

B = C ) implies B is a_partition of Y )

assume that

A1: B c= H and

A2: for C being mutually-disjoint Subset-Family of Y st C c= H & union B c= union C holds

B = C ; :: thesis: B is a_partition of Y

thus union B = Y by A1, A2, Lm3; :: according to EQREL_1:def 4 :: thesis: for b_{1} being Element of bool Y holds

( not b_{1} in B or ( not b_{1} = {} & ( for b_{2} being Element of bool Y holds

( not b_{2} in B or b_{1} = b_{2} or b_{1} misses b_{2} ) ) ) )

thus for b_{1} being Element of bool Y holds

( not b_{1} in B or ( not b_{1} = {} & ( for b_{2} being Element of bool Y holds

( not b_{2} in B or b_{1} = b_{2} or b_{1} misses b_{2} ) ) ) )
by A1, A2, Def5, Lm4; :: thesis: verum

for B being mutually-disjoint Subset-Family of Y st B c= H & ( for C being mutually-disjoint Subset-Family of Y st C c= H & union B c= union C holds

B = C ) holds

B is a_partition of Y

let H be covering Hierarchy of Y; :: thesis: for B being mutually-disjoint Subset-Family of Y st B c= H & ( for C being mutually-disjoint Subset-Family of Y st C c= H & union B c= union C holds

B = C ) holds

B is a_partition of Y

let B be mutually-disjoint Subset-Family of Y; :: thesis: ( B c= H & ( for C being mutually-disjoint Subset-Family of Y st C c= H & union B c= union C holds

B = C ) implies B is a_partition of Y )

assume that

A1: B c= H and

A2: for C being mutually-disjoint Subset-Family of Y st C c= H & union B c= union C holds

B = C ; :: thesis: B is a_partition of Y

thus union B = Y by A1, A2, Lm3; :: according to EQREL_1:def 4 :: thesis: for b

( not b

( not b

thus for b

( not b

( not b