assume not { F₂(a) where a is Element of F₁() : P₁[a] } = {} ; :: thesis: contradiction
then reconsider X = { F₂(a) where a is Element of F₁() : P₁[a] } as non empty set ;
set x = the Element of X;
the Element of X in X ;
then ex a being Element of F₁() st
( the Element of X = F₂(a) & P₁[a] ) ;
hence contradiction by A1; :: thesis: verum