F is GeneratorSet of F

proof

thus F = uparrow (fininfs F) by Lm3; :: according to WAYBEL12:def 3 :: thesis: verum

end;

then reconsider F1 = F as GeneratorSet of F ;
take F1 ; :: thesis: not F1 is empty
thus not F1 is empty ; :: thesis: verum