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₁ being Element of bool Y holds
( not b₁ in B or ( not b₁ = {} & ( for b₂ being Element of bool Y holds
( not b₂ in B or b₁ = b₂ or b₁ misses b₂ ) ) ) )
thus for b₁ being Element of bool Y holds
( not b₁ in B or ( not b₁ = {} & ( for b₂ being Element of bool Y holds
( not b₂ in B or b₁ = b₂ or b₁ misses b₂ ) ) ) ) by A1, A2, Def5, Lm4; :: thesis: verum