theorem LmCommutative1: :: EC_PF_3:17

for p being 5 _or_greater Prime
for z being Element of EC_WParam p
for P, Q, O, PQ, QP being Element of EC_SetProjCo ((z `1),(z `2),p) st O = [0,1,0] & not P _EQ_ O & not Q _EQ_ O & not P _EQ_ Q & PQ = (addell_ProjCo (z,p)) . (P,Q) & QP = (addell_ProjCo (z,p)) . (Q,P) holds
( QP `1_3 = - (PQ `1_3) & QP `2_3 = - (PQ `2_3) & QP `3_3 = - (PQ `3_3) )