theorem Th23: :: ORTSP_1:23

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