set X = { F₄(x,y) where x is Element of F₁(), y is Element of F₂() : P₁[x,y] } ;
{ F₄(x,y) where x is Element of F₁(), y is Element of F₂() : P₁[x,y] } c= F₃()

proof

let w be set ; :: according to TARSKI:def 3 :: thesis: ( not w in { F₄(x,y) where x is Element of F₁(), y is Element of F₂() : P₁[x,y] } or w in F₃() )
assume w in { F₄(x,y) where x is Element of F₁(), y is Element of F₂() : P₁[x,y] } ; :: thesis: w in F₃()
then ex x being Element of F₁() ex y being Element of F₂() st
( w = F₄(x,y) & P₁[x,y] ) ;
hence w in F₃() ; :: thesis: verum

end;

hence { F₄(x,y) where x is Element of F₁(), y is Element of F₂() : P₁[x,y] } is Subset of F₃() ; :: thesis: verum