:: deftheorem Def6 defines pcs-InternalRels PCS_0:def 6 :
for I being non empty set
for C being RelStr-yielding ManySortedSet of I
for b₃ being ManySortedSet of I holds
( b₃ = pcs-InternalRels C iff for i being Element of I holds b₃ . i = the InternalRel of (C . i) );