theorem Th7: :: ORTSP_1:7

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