thus rng (XFS2FS ((PrimeNumbersS s) | s)) c= SetPrimes by RELAT_1:def 19; :: according to FINSEQ_1:def 4 :: thesis: verum