theorem Th9: :: ORTSP_1:9

for F being Field
for S being OrtSp of F
for a, b being Element of S st a _|_ & b _|_ holds
a - b _|_