len (PrimeNumbersFS s) = s by Th42;
hence not PrimeNumbersFS s is empty ; :: thesis: verum