:: deftheorem defines psInt DECOMP_1:def 9 :
for T being TopStruct
for B being Subset of T holds psInt B = B /\ (Cl (Int (Cl B)));