F = uparrow (fininfs F) by Lm3;
then reconsider F1 = F as GeneratorSet of F by Def3;
take F1 ; :: thesis: not F1 is empty
thus not F1 is empty ; :: thesis: verum