assume { F₃(y) where y is Element of F₁() : ( P₁[y] & not F₃(y) in F₂() ) } meets F₂() ; :: thesis: contradiction
then consider x being object such that
A1: x in { F₃(y) where y is Element of F₁() : ( P₁[y] & not F₃(y) in F₂() ) } and
A2: 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 A2; :: thesis: verum