theorem Th3: :: ORTSP_1:3

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