:: deftheorem Def5 defines pcs-InternalRels PCS_0:def 5 :
for I being set
for C being RelStr-yielding ManySortedSet of I
for b₃ being ManySortedSet of I holds
( b₃ = pcs-InternalRels C iff for i being set st i in I holds
ex P being RelStr st
( P = C . i & b₃ . i = the InternalRel of P ) );