{ x where x is Element of F₁() : P₁[x] } is Subset of F₁() from DOMAIN_1:sch 7();
hence { x where x is Element of F₁() : P₁[x] } c= F₁() ; :: thesis: verum