scheme :: SUBSET_1:sch 1
SubsetEx{ F1() -> set , P1[ object ] } :
ex X being Subset of F1() st
for x being set holds
( x in X iff ( x in F1() & P1[x] ) )