reconsider S = { F₃(x) where x is Element of F₁() : P₁[x] } as Subset of F₂() from DOMAIN_1:sch 8();
take S ; :: thesis: S = { F₃(x) where x is Element of F₁() : P₁[x] }
thus S = { F₃(x) where x is Element of F₁() : P₁[x] } ; :: thesis: verum