theorem Th31: :: SYMSP_1:31

for F being Field
for S being SymSp of F
for a, p, x, y being Element of S st not p _|_ & not p _|_ & not p _|_ holds
(ProJ (p,a,x)) * (ProJ (x,p,y)) = (- (ProJ (p,a,y))) * (ProJ (y,p,x))