theorem Th1: :: ORTSP_1:1
for F being Field
for S being OrtSp of F
for a being Element of S holds a _|_