let p be Prime; :: thesis: for a, b being Element of (GF p) st p > 3 & Disc (a,b,p) <> 0. (GF p) holds
Class (R_EllCur (a,b,p)) = {(Class ((R_EllCur (a,b,p)),[0,1,0]))} \/ { (Class ((R_EllCur (a,b,p)),P)) where P is Element of ProjCo (GF p) : ( P in EC_SetProjCo (a,b,p) & ex X, Y being Element of (GF p) st P = [X,Y,1] ) }
let a, b be Element of (GF p); :: thesis: ( p > 3 & Disc (a,b,p) <> 0. (GF p) implies Class (R_EllCur (a,b,p)) = {(Class ((R_EllCur (a,b,p)),[0,1,0]))} \/ { (Class ((R_EllCur (a,b,p)),P)) where P is Element of ProjCo (GF p) : ( P in EC_SetProjCo (a,b,p) & ex X, Y being Element of (GF p) st P = [X,Y,1] ) } )
assume AS: ( p > 3 & Disc (a,b,p) <> 0. (GF p) ) ; :: thesis: Class (R_EllCur (a,b,p)) = {(Class ((R_EllCur (a,b,p)),[0,1,0]))} \/ { (Class ((R_EllCur (a,b,p)),P)) where P is Element of ProjCo (GF p) : ( P in EC_SetProjCo (a,b,p) & ex X, Y being Element of (GF p) st P = [X,Y,1] ) }
set A = Class (R_EllCur (a,b,p));
set B = {(Class ((R_EllCur (a,b,p)),[0,1,0]))} \/ { (Class ((R_EllCur (a,b,p)),P)) where P is Element of ProjCo (GF p) : ( P in EC_SetProjCo (a,b,p) & ex X, Y being Element of (GF p) st P = [X,Y,1] ) } ;
reconsider d0 = [0,1,0] as Element of EC_SetProjCo (a,b,p) by ECZERO;
for x being set holds
( x in Class (R_EllCur (a,b,p)) iff x in {(Class ((R_EllCur (a,b,p)),[0,1,0]))} \/ { (Class ((R_EllCur (a,b,p)),P)) where P is Element of ProjCo (GF p) : ( P in EC_SetProjCo (a,b,p) & ex X, Y being Element of (GF p) st P = [X,Y,1] ) } )

proof

let x be set ; :: thesis: ( x in Class (R_EllCur (a,b,p)) iff x in {(Class ((R_EllCur (a,b,p)),[0,1,0]))} \/ { (Class ((R_EllCur (a,b,p)),P)) where P is Element of ProjCo (GF p) : ( P in EC_SetProjCo (a,b,p) & ex X, Y being Element of (GF p) st P = [X,Y,1] ) } )

hereby :: thesis: ( x in {(Class ((R_EllCur (a,b,p)),[0,1,0]))} \/ { (Class ((R_EllCur (a,b,p)),P)) where P is Element of ProjCo (GF p) : ( P in EC_SetProjCo (a,b,p) & ex X, Y being Element of (GF p) st P = [X,Y,1] ) } implies x in Class (R_EllCur (a,b,p)) )

assume x in Class (R_EllCur (a,b,p)) ; :: thesis: x in {(Class ((R_EllCur (a,b,p)),[0,1,0]))} \/ { (Class ((R_EllCur (a,b,p)),P)) where P is Element of ProjCo (GF p) : ( P in EC_SetProjCo (a,b,p) & ex X, Y being Element of (GF p) st P = [X,Y,1] ) }
then ( ex y being Element of ProjCo (GF p) st
( y in EC_SetProjCo (a,b,p) & y = [0,1,0] & x = Class ((R_EllCur (a,b,p)),y) ) or ex y being Element of ProjCo (GF p) ex e, f being Element of (GF p) st
( y in EC_SetProjCo (a,b,p) & y = [e,f,1] & x = Class ((R_EllCur (a,b,p)),y) ) ) by AS, LmDefREQ3;
then ( x in {(Class ((R_EllCur (a,b,p)),[0,1,0]))} or x in { (Class ((R_EllCur (a,b,p)),y)) where y is Element of ProjCo (GF p) : ( y in EC_SetProjCo (a,b,p) & ex e, f being Element of (GF p) st y = [e,f,1] ) } ) by TARSKI:def 1;
hence x in {(Class ((R_EllCur (a,b,p)),[0,1,0]))} \/ { (Class ((R_EllCur (a,b,p)),P)) where P is Element of ProjCo (GF p) : ( P in EC_SetProjCo (a,b,p) & ex X, Y being Element of (GF p) st P = [X,Y,1] ) } by XBOOLE_0:def 3; :: thesis: verum

end;

assume x in {(Class ((R_EllCur (a,b,p)),[0,1,0]))} \/ { (Class ((R_EllCur (a,b,p)),P)) where P is Element of ProjCo (GF p) : ( P in EC_SetProjCo (a,b,p) & ex X, Y being Element of (GF p) st P = [X,Y,1] ) } ; :: thesis: x in Class (R_EllCur (a,b,p))
then P1: ( x in {(Class ((R_EllCur (a,b,p)),[0,1,0]))} or x in { (Class ((R_EllCur (a,b,p)),y)) where y is Element of ProjCo (GF p) : ( y in EC_SetProjCo (a,b,p) & ex e, f being Element of (GF p) st y = [e,f,1] ) } ) by XBOOLE_0:def 3;

now

per cases ( x = Class ((R_EllCur (a,b,p)),[0,1,0]) or ex y being Element of ProjCo (GF p) st
( x = Class ((R_EllCur (a,b,p)),y) & y in EC_SetProjCo (a,b,p) & ex e, f being Element of (GF p) st y = [e,f,1] ) ) by P1, TARSKI:def 1;

suppose AD1: x = Class ((R_EllCur (a,b,p)),[0,1,0]) ; :: thesis: x in Class (R_EllCur (a,b,p))

EqClass ((R_EllCur (a,b,p)),d0) is Element of Class (R_EllCur (a,b,p)) ;
hence x in Class (R_EllCur (a,b,p)) by AD1; :: thesis: verum

end;

suppose ex y being Element of ProjCo (GF p) st
( x = Class ((R_EllCur (a,b,p)),y) & y in EC_SetProjCo (a,b,p) & ex e, f being Element of (GF p) st y = [e,f,1] ) ; :: thesis: x in Class (R_EllCur (a,b,p))

then consider y being Element of ProjCo (GF p) such that
AD3: ( x = Class ((R_EllCur (a,b,p)),y) & y in EC_SetProjCo (a,b,p) & ex e, f being Element of (GF p) st y = [e,f,1] ) ;
reconsider y = y as Element of EC_SetProjCo (a,b,p) by AD3;
EqClass ((R_EllCur (a,b,p)),y) is Element of Class (R_EllCur (a,b,p)) ;
hence x in Class (R_EllCur (a,b,p)) by AD3; :: thesis: verum

end;

end;

end;

hence x in Class (R_EllCur (a,b,p)) ; :: thesis: verum

end;

hence Class (R_EllCur (a,b,p)) = {(Class ((R_EllCur (a,b,p)),[0,1,0]))} \/ { (Class ((R_EllCur (a,b,p)),P)) where P is Element of ProjCo (GF p) : ( P in EC_SetProjCo (a,b,p) & ex X, Y being Element of (GF p) st P = [X,Y,1] ) } by TARSKI:1; :: thesis: verum