assume { F₃(y) where y is Element of F₁() : ( P₁[y] & not F₃(y) in F₂() ) } meets F₂() ; :: thesis: contradiction
then consider x being set such that
A1: ( x in { F₃(y) where y is Element of F₁() : ( P₁[y] & not F₃(y) in F₂() ) } & x in F₂() ) by XBOOLE_0:3;
ex y being Element of F₁() st
( x = F₃(y) & P₁[y] & not F₃(y) in F₂() ) by A1;
hence contradiction by A1; :: thesis: verum