scheme :: SUBSET_1:sch 1
SubsetEx{ F₁() -> set , P₁[ object ] } :

ex X being Subset of F₁() st
for x being set holds
( x in X iff ( x in F₁() & P₁[x] ) )