theorem :: PCS_0:42

for P being RelStr
for D being Subset-Family of P
for A, B being set holds
( [A,B] in pcs-general-power-IR (P,D) iff ( A in D & B in D & ( for a being Element of P st a in A holds
ex b being Element of P st
( b in B & a <= b ) ) ) )