let p be 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
let a, b be 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
let P be Element of ProjCo (GF p); ( ( P = [0,1,0] or P `3_3 = 1 ) implies rep_pt P = P )
A1:
( P = [0,1,0] implies rep_pt P = P )
( P `3_3 = 1 implies rep_pt P = P )
hence
( ( P = [0,1,0] or P `3_3 = 1 ) implies rep_pt P = P )
by A1; verum