scheme :: DOMAIN_1:sch 1
Fraenkel1{ P₁[ object ] } :

for X1 being non empty set holds { x1 where x1 is Element of X1 : P₁[x1] } is Subset of X1