let h, i be Integer; :: thesis: ( i in PrimeDivisors>3 h implies i > 3 )
assume i in PrimeDivisors>3 h ; :: thesis: i > 3
then i >= 3 + 1 by NUMBER09:56;
hence i > 3 by NAT_1:13; :: thesis: verum