pcs-coherent-power P is pcs-self-coherent-membered

proof

let S be Subset of P; :: according to PCS_0:def 44 :: thesis: ( S in pcs-coherent-power P implies S is pcs-self-coherent )
thus ( S in pcs-coherent-power P implies S is pcs-self-coherent ) by Th48; :: thesis: verum

end;

hence for b₁ being Subset-Family of P st b₁ = pcs-coherent-power P holds
b₁ is pcs-self-coherent-membered ; :: thesis: verum