{ n where n is Prime : n is fermat } c= SetPrimes

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { n where n is Prime : n is fermat } or x in SetPrimes )
assume x in { n where n is Prime : n is fermat } ; :: thesis: x in SetPrimes
then consider n being Prime such that
A1: ( n = x & n is fermat ) ;
thus x in SetPrimes by A1, NEWTON:def 6; :: thesis: verum

end;

hence Fermat_Primes c= SetPrimes ; :: thesis: verum