theorem Th29: :: YELLOW14:29

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