:: deftheorem Def5 defines without_boundary MFOLD_0:def 5 :
for M being non empty locally_euclidean TopSpace holds
( M is without_boundary iff Int M = the carrier of M );