theorem Th6: :: ORTSP_1:6

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