:: deftheorem defines spInt DECOMP_1:def 10 :
for T being TopStruct
for B being Subset of T holds spInt B = (sInt B) \/ (pInt B);