theorem Th26: :: ORTSP_1:26

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