{ F₂(s,t) where s, t is Element of F₁() : P₁[s,t] } c= F₁()

proof

let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in { F₂(s,t) where s, t is Element of F₁() : P₁[s,t] } or q in F₁() )
assume q in { F₂(s,t) where s, t is Element of F₁() : P₁[s,t] } ; :: thesis: q in F₁()
then ex s, t being Element of F₁() st
( q = F₂(s,t) & P₁[s,t] ) ;
hence q in F₁() by A1; :: thesis: verum

end;

hence { F₂(s,t) where s, t is Element of F₁() : P₁[s,t] } is Subset of F₁() ; :: thesis: verum