scheme :: INT_1:sch 1
SepInt{ P1[ Integer] } :
ex X being Subset of INT st
for x being Integer holds
( x in X iff P1[x] )