consider a0 being object such that
A1: a0 in F₁() by XBOOLE_0:def 1;
F₂(a0) in { F₂(a) where a is Element of F₁() : verum } by A1;
hence not { F₂(a) where a is Element of F₁() : verum } is empty ; :: thesis: verum