theorem Th8: :: ORTSP_1:8

for F being Field
for S being OrtSp of F
for a, b, x being Element of S
for k, l being Element of F st not a _|_ & a _|_ & a _|_ holds
k = l