scheme :: INT_1:sch 1
SepInt{ P₁[ Integer] } :

ex X being Subset of INT st
for x being Integer holds
( x in X iff P₁[x] )