let p be 5 _or_greater Prime; :: thesis: for z being Element of EC_WParam p holds
( p > 3 & Disc ((z `1),(z `2),p) <> 0. (GF p) )
let z be Element of EC_WParam p; :: thesis: ( p > 3 & Disc ((z `1),(z `2),p) <> 0. (GF p) )
p >= 4 + 1 by Def1;
hence p > 3 by XXREAL_0:2; :: thesis: Disc ((z `1),(z `2),p) <> 0. (GF p)
z in { [a,b] where a, b is Element of (GF p) : Disc (a,b,p) <> 0. (GF p) } ;
then consider a, b being Element of (GF p) such that
A1: ( z = [a,b] & Disc (a,b,p) <> 0. (GF p) ) ;
thus Disc ((z `1),(z `2),p) <> 0. (GF p) by A1; :: thesis: verum