theorem Th27: :: SYMSP_1:27

for F being Field
for S being SymSp of F
for a, b, c being Element of S st not b _|_ & not b _|_ holds
ProJ (c,b,a) = (- ((ProJ (b,a,c)) ")) * (ProJ (a,b,c))