let P be pcs-Str ; :: thesis: for X being set st X in pcs-coherent-power P holds
X is pcs-self-coherent Subset of P
let X be set ; :: thesis: ( X in pcs-coherent-power P implies X is pcs-self-coherent Subset of P )
assume X in pcs-coherent-power P ; :: thesis: X is pcs-self-coherent Subset of P
then ex Y being Subset of P st
( X = Y & Y is pcs-self-coherent ) ;
hence X is pcs-self-coherent Subset of P ; :: thesis: verum