let h, i be Integer; :: thesis: ( i in PrimeDivisors>3 h implies i is prime )
assume i in PrimeDivisors>3 h ; :: thesis: i is prime
then i in PrimeDivisors h ;
then ex p being Prime st
( i = p & p divides h ) ;
hence i is prime ; :: thesis: verum