theorem Th27: :: ORTSP_1:27

for F being Field
for S being OrtSp 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))