theorem Th20: :: ORTSP_1:20

for F being Field
for S being OrtSp of F
for a, b, x being Element of S st not a _|_ holds
( a _|_ iff ProJ (a,b,x) = 0. F )