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