:: deftheorem defines Fr ISOMICHI:def 4 :
for T being TopStruct
for A being Subset of T holds Fr A = (Cl A) \ (Int A);