len (primesFinS 0) = 0 by Def1;
hence primesFinS 0 is empty ; :: thesis: verum