theorem Th48: :: PCS_0:48

for P being pcs-Str
for X being set st X in pcs-coherent-power P holds
X is pcs-self-coherent Subset of P