theorem LemmaDivides: :: NUMBER06:1

for p being Prime st 3 divides p holds
p = 3 by INT_2:def 4;