theorem Th9: :: SYMSP_1:9

for F being Field
for S being SymSp of F
for a, b being Element of S st a <> 0. S & b <> 0. S holds
ex p being Element of S st
( not a _|_ & not b _|_ )