:: deftheorem defines PrimeDivisors>3 NUMBER14:def 11 :
for h being Integer holds PrimeDivisors>3 h = (PrimeDivisors h) /\ (GreaterOrEqualsNumbers 4);