take F = {{}} .--> {{}}; :: thesis: ( not F is empty & F is finite-yielding )
thus not F is empty ; :: thesis: F is finite-yielding
let x be object ; :: according to FINSET_1:def 5 :: thesis: ( x in {{{}}} implies F . x is finite )
assume x in {{{}}} ; :: thesis: F . x is finite
then x = {{}} by TARSKI:def 1;
hence F . x is finite by FUNCOP_1:72; :: thesis: verum