theorem Th8: :: MFOLD_0:8

for N, M being non empty locally_euclidean TopSpace holds Int [:N,M:] = [:(Int N),(Int M):]