theorem Th6: :: MFOLD_0:5

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