consider a0 being object such that

A1: a0 in F_{1}()
by XBOOLE_0:def 1;

F_{2}(a0) in { F_{2}(a) where a is Element of F_{1}() : verum }
by A1;

hence not { F_{2}(a) where a is Element of F_{1}() : verum } is empty
; :: thesis: verum

A1: a0 in F

F

hence not { F