theorem Th46: :: EC_PF_1:46

for p being Prime
for P, Q being Element of ProjCo (GF p) holds
( P _EQ_ Q iff [P,Q] in R_ProjCo p )