:: deftheorem defines EC_WParam EC_PF_2:def 2 :
for p being 5 _or_greater Prime holds EC_WParam p = { [a,b] where a, b is Element of (GF p) : Disc (a,b,p) <> 0. (GF p) } ;