theorem Th30: :: EC_PF_2:30

for p being 5 _or_greater Prime
for z being Element of EC_WParam p holds
( p > 3 & Disc ((z `1),(z `2),p) <> 0. (GF p) )