theorem :: SYMSP_1:34

for F being Field
for S being SymSp of F
for a, b, x, y being Element of S st (1_ F) + (1_ F) <> 0. F & not a _|_ holds
PProJ (a,b,x,y) = - (PProJ (a,b,y,x))