:: deftheorem defines Border ISOMICHI:def 5 :
for T being TopStruct
for A being Subset of T holds Border A = Int (Fr A);