theorem ThRepPoint5: :: EC_PF_3:1

for p being Prime
for a, b being Element of (GF p)
for P being Element of ProjCo (GF p) st ( P = [0,1,0] or P `3_3 = 1 ) holds
rep_pt P = P