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