:: deftheorem Def45 defines pcs-general-power-IR PCS_0:def 46 :
for P being RelStr
for D being set
for b₃ being Relation of D holds
( b₃ = pcs-general-power-IR (P,D) iff for A, B being set holds
( [A,B] in b₃ iff ( A in D & B in D & ( for a being set st a in A holds
ex b being set st
( b in B & [a,b] in the InternalRel of P ) ) ) ) );