theorem Th53: :: EC_PF_1:53

for p being Prime
for a, b being Element of (GF p)
for F1, F2 being set st p > 3 & Disc (a,b,p) <> 0. (GF p) & F1 = {(Class ((R_EllCur (a,b,p)),[0,1,0]))} & F2 = { (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] ) } holds
F1 misses F2