theorem Ttool7a: :: XPRIMET1:5

for p being Prime holds
( not p < 7 or p = 2 or p = 3 or p = 5 )