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