let p be Prime; :: thesis: for a, b being Element of (GF p)
for x being set st p > 3 & Disc (a,b,p) <> 0. (GF p) & x in Class (R_EllCur (a,b,p)) & ( for P being Element of ProjCo (GF p) holds
( not P in EC_SetProjCo (a,b,p) or not P = [0,1,0] or not x = Class ((R_EllCur (a,b,p)),P) ) ) holds
ex P being Element of ProjCo (GF p) ex X, Y being Element of (GF p) st
( P in EC_SetProjCo (a,b,p) & P = [X,Y,1] & x = Class ((R_EllCur (a,b,p)),P) )
let a, b be Element of (GF p); :: thesis: for x being set st p > 3 & Disc (a,b,p) <> 0. (GF p) & x in Class (R_EllCur (a,b,p)) & ( for P being Element of ProjCo (GF p) holds
( not P in EC_SetProjCo (a,b,p) or not P = [0,1,0] or not x = Class ((R_EllCur (a,b,p)),P) ) ) holds
ex P being Element of ProjCo (GF p) ex X, Y being Element of (GF p) st
( P in EC_SetProjCo (a,b,p) & P = [X,Y,1] & x = Class ((R_EllCur (a,b,p)),P) )
let x be set ; :: thesis: ( p > 3 & Disc (a,b,p) <> 0. (GF p) & x in Class (R_EllCur (a,b,p)) & ( for P being Element of ProjCo (GF p) holds
( not P in EC_SetProjCo (a,b,p) or not P = [0,1,0] or not x = Class ((R_EllCur (a,b,p)),P) ) ) implies ex P being Element of ProjCo (GF p) ex X, Y being Element of (GF p) st
( P in EC_SetProjCo (a,b,p) & P = [X,Y,1] & x = Class ((R_EllCur (a,b,p)),P) ) )
assume AS1: ( p > 3 & Disc (a,b,p) <> 0. (GF p) & x in Class (R_EllCur (a,b,p)) ) ; :: thesis: ( ex P being Element of ProjCo (GF p) st
( P in EC_SetProjCo (a,b,p) & P = [0,1,0] & x = Class ((R_EllCur (a,b,p)),P) ) or ex P being Element of ProjCo (GF p) ex X, Y being Element of (GF p) st
( P in EC_SetProjCo (a,b,p) & P = [X,Y,1] & x = Class ((R_EllCur (a,b,p)),P) ) )
then consider y0 being Element of EC_SetProjCo (a,b,p) such that
P1: x = Class ((R_EllCur (a,b,p)),y0) by EQREL_1:36;
reconsider w = y0 as Element of ProjCo (GF p) ;

per cases ( w `3 = 0 or w `3 <> 0 ) ;

suppose w `3 = 0 ; :: thesis: ( ex P being Element of ProjCo (GF p) st
( P in EC_SetProjCo (a,b,p) & P = [0,1,0] & x = Class ((R_EllCur (a,b,p)),P) ) or ex P being Element of ProjCo (GF p) ex X, Y being Element of (GF p) st
( P in EC_SetProjCo (a,b,p) & P = [X,Y,1] & x = Class ((R_EllCur (a,b,p)),P) ) )

then consider y being Element of ProjCo (GF p) such that
D2: ( y in EC_SetProjCo (a,b,p) & y _EQ_ w & y `1 = 0 & y `2 = 1 & y `3 = 0 ) by AS1, LmDefREQ2;
[y,w] in R_EllCur (a,b,p) by AS1, LmDefREQ0, D2;
then x = Class ((R_EllCur (a,b,p)),y) by P1, D2, EQREL_1:35;
hence ( ex P being Element of ProjCo (GF p) st
( P in EC_SetProjCo (a,b,p) & P = [0,1,0] & x = Class ((R_EllCur (a,b,p)),P) ) or ex P being Element of ProjCo (GF p) ex X, Y being Element of (GF p) st
( P in EC_SetProjCo (a,b,p) & P = [X,Y,1] & x = Class ((R_EllCur (a,b,p)),P) ) ) by D2, MCART_1:44; :: thesis: verum

end;

suppose w `3 <> 0 ; :: thesis: ( ex P being Element of ProjCo (GF p) st
( P in EC_SetProjCo (a,b,p) & P = [0,1,0] & x = Class ((R_EllCur (a,b,p)),P) ) or ex P being Element of ProjCo (GF p) ex X, Y being Element of (GF p) st
( P in EC_SetProjCo (a,b,p) & P = [X,Y,1] & x = Class ((R_EllCur (a,b,p)),P) ) )

then consider y being Element of ProjCo (GF p) such that
D2: ( y in EC_SetProjCo (a,b,p) & y _EQ_ w & y `3 = 1 ) by AS1, LmDefREQ1;
set e = y `1 ;
set f = y `2 ;
F1: y = [(y `1),(y `2),1] by D2, MCART_1:44;
[y,w] in R_EllCur (a,b,p) by AS1, LmDefREQ0, D2;
then x = Class ((R_EllCur (a,b,p)),y) by P1, D2, EQREL_1:35;
hence ( ex P being Element of ProjCo (GF p) st
( P in EC_SetProjCo (a,b,p) & P = [0,1,0] & x = Class ((R_EllCur (a,b,p)),P) ) or ex P being Element of ProjCo (GF p) ex X, Y being Element of (GF p) st
( P in EC_SetProjCo (a,b,p) & P = [X,Y,1] & x = Class ((R_EllCur (a,b,p)),P) ) ) by F1, D2; :: thesis: verum

end;

end;