pcs-coherent-power P c= bool the carrier of P
proof
let X be object ; :: according to TARSKI:def 3 :: thesis: ( not X in pcs-coherent-power P or X in bool the carrier of P )
assume X in pcs-coherent-power P ; :: thesis: X in bool the carrier of P
then X is Subset of P by Th48;
hence X in bool the carrier of P ; :: thesis: verum
end;
hence pcs-coherent-power P is Subset-Family of P ; :: thesis: verum