theorem Th46: :: PCS_0:46

for P being pcs-Str
for D being set
for p, q being Element of (pcs-general-power (P,D)) st p (--) q holds
for p9, q9 being Element of P st p9 in p & q9 in q holds
p9 (--) q9 by Def46;