:: deftheorem defines Fr MFOLD_0:def 4 :
for M being non empty locally_euclidean TopSpace holds Fr M = (Int M) ` ;