let x be object ; :: thesis: ( x in Fermat_Primes implies x is fermat Prime )
assume x in Fermat_Primes ; :: thesis: x is fermat Prime
then consider n being Prime such that
A1: ( n = x & n is fermat ) ;
thus x is fermat Prime by A1; :: thesis: verum