theorem :: PCS_0:43

for P being TolStr
for D being Subset-Family of P
for A, B being set holds
( [A,B] in pcs-general-power-TR (P,D) iff ( A in D & B in D & ( for a, b being Element of P st a in A & b in B holds
a (--) b ) ) )