for n being Element of NAT
for C being non empty Poset
for A being non empty Element of symplexes C st card A = n holds
dom (SgmX ( the InternalRel of C,A)) = Seg n