let h, i be Integer; :: thesis: ( i is prime & i > 3 & i divides h implies i in PrimeDivisors>3 h )
assume that
A1: i is prime and
A2: i > 3 and
A3: i divides h ; :: thesis: i in PrimeDivisors>3 h
A4: i is Element of NAT by A2, INT_1:3;
then A5: i in PrimeDivisors h by A1, A3;
i >= 3 + 1 by A2, NAT_1:13;
then i in GreaterOrEqualsNumbers 4 by A4, NUMBER09:56;
hence i in PrimeDivisors>3 h by A5, XBOOLE_0:def 4; :: thesis: verum