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