scheme :: SUBSET_1:sch 3
SubsetEx{ F1() -> non empty set , P1[ object ] } :
ex B being Subset of F1() st
for x being Element of F1() holds
( x in B iff P1[x] )