theorem Th31: :: YELLOW14:31

for M being non empty set
for i being Element of M
for J being non-Empty TopStruct-yielding ManySortedSet of M
for x being Point of (product J) holds pi ((Cl {x}),i) = Cl {(x . i)}