theorem Th1: :: IRRAT_1:1

for p being Nat st p is prime holds
sqrt p is irrational