for F being Field
for S being OrtSp of F st (1_ F) + (1_ F) <> 0. F & ex a being Element of S st a <> 0. S holds
ex b being Element of S st not b _|_